Theorem rabn0 4412

Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999.) (Revised by BJ, 16-Jul-2021.)

Assertion

Ref	Expression
rabn0	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem rabn0

Step	Hyp	Ref	Expression
1		rabeq0 4411	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	necon3abii 2993	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3		dfrex2 3079	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitr4i 278	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2946  ∀wral 3067  ∃wrex 3076  {crab 3443  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-dif 3979  df-nul 4353

This theorem is referenced by:  class2set  5373  reusv2  5421  exss  5483  frminex  5679  weniso  7390  onminesb  7829  onminsb  7830  onminex  7838  oeeulem  8657  supval2  9524  ordtypelem3  9589  card2on  9623  tz9.12lem3  9858  rankf  9863  scott0  9955  karden  9964  cardf2  10012  cardval3  10021  cardmin2  10068  acni3  10116  kmlem3  10222  cofsmo  10338  coftr  10342  fin23lem7  10385  enfin2i  10390  axcc4  10508  axdc3lem4  10522  ac6num  10548  pwfseqlem3  10729  wuncval  10811  wunccl  10813  tskmcl  10910  infm3  12254  nnwos  12980  zsupss  13002  zmin  13009  rpnnen1lem2  13042  rpnnen1lem1  13043  rpnnen1lem3  13044  rpnnen1lem5  13046  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  bitsfzolem  16480  lcmcllem  16643  fissn0dvdsn0  16667  odzcllem  16839  vdwnn  17045  ram0  17069  ramsey  17077  sylow2blem3  19664  iscyg2  19924  pgpfac1lem5  20123  ablfaclem2  20130  ablfaclem3  20131  ablfac  20132  lspf  20995  ordtrest2lem  23232  ordthauslem  23412  1stcfb  23474  2ndcdisj  23485  ptclsg  23644  txconn  23718  txflf  24035  tsmsfbas  24157  iscmet3  25346  minveclem3b  25481  iundisj  25602  dyadmax  25652  dyadmbllem  25653  elqaalem1  26379  elqaalem3  26381  sgmnncl  27208  musum  27252  conway  27862  incistruhgr  29114  uvtx01vtx  29432  spancl  31368  shsval2i  31419  ococin  31440  iundisjf  32611  iundisjfi  32801  ordtrest2NEWlem  33868  esumrnmpt2  34032  esumpinfval  34037  dmsigagen  34108  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemsup  34469  bnj110  34834  bnj1204  34988  bnj1253  34993  connpconn  35203  iscvm  35227  wsuclem  35789  weiunlem2  36429  poimirlem28  37608  sstotbnd2  37734  igenval  38021  igenidl  38023  pmap0  39722  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8  42044  grpods  42151  unitscyglem3  42154  unitscyglem4  42155  fsuppind  42545  pellfundre  42837  pellfundge  42838  pellfundglb  42841  dgraalem  43102  rgspncl  43126  uzwo4  44955  ioodvbdlimc1lem1  45852  fourierdlem31  46059  fourierdlem64  46091  etransclem48  46203  subsaliuncl  46279  smflimlem6  46697  smfpimcc  46729  prmdvdsfmtnof1lem1  47458  prmdvdsfmtnof  47460