Theorem rabn0 4186

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 4185	. . 3 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
2	1	necon3abii 3044	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
3		dfrex2 3203	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ¬ ∀𝑥 ∈ 𝐴 ¬ 𝜑)
4	2, 3	bitr4i 270	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 198   ≠ wne 2998  ∀wral 3116  ∃wrex 3117  {crab 3120  ∅c0 4143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-ral 3121  df-rex 3122  df-rab 3125  df-v 3415  df-dif 3800  df-nul 4144

This theorem is referenced by:  class2set  5053  reusv2  5102  exss  5151  frminex  5321  weniso  6858  onminesb  7258  onminsb  7259  onminex  7267  oeeulem  7947  supval2  8629  ordtypelem3  8693  card2on  8727  tz9.12lem3  8928  rankf  8933  scott0  9025  karden  9034  cardf2  9081  cardval3  9090  cardmin2  9136  acni3  9182  kmlem3  9288  cofsmo  9405  coftr  9409  fin23lem7  9452  enfin2i  9457  axcc4  9575  axdc3lem4  9589  ac6num  9615  pwfseqlem3  9796  wuncval  9878  wunccl  9880  tskmcl  9977  infm3  11311  nnwos  12037  zsupss  12059  zmin  12066  rpnnen1lem2  12098  rpnnen1lem1  12099  rpnnen1lem3  12100  rpnnen1lem5  12102  ioo0  12487  ico0  12508  ioc0  12509  icc0  12510  bitsfzolem  15528  lcmcllem  15681  fissn0dvdsn0  15705  odzcllem  15867  vdwnn  16072  ram0  16096  ramsey  16104  sylow2blem3  18387  iscyg2  18636  pgpfac1lem5  18831  ablfaclem2  18838  ablfaclem3  18839  ablfac  18840  lspf  19332  ordtrest2lem  21377  ordthauslem  21557  1stcfb  21618  2ndcdisj  21629  ptclsg  21788  txconn  21862  txflf  22179  tsmsfbas  22300  iscmet3  23460  minveclem3b  23595  iundisj  23713  dyadmax  23763  dyadmbllem  23764  elqaalem1  24472  elqaalem3  24474  sgmnncl  25285  musum  25329  incistruhgr  26376  uvtx01vtx  26694  spancl  28749  shsval2i  28800  ococin  28821  iundisjf  29948  iundisjfi  30101  ordtrest2NEWlem  30512  esumrnmpt2  30674  esumpinfval  30679  dmsigagen  30751  ballotlemfc0  31099  ballotlemfcc  31100  ballotlemiex  31108  ballotlemsup  31111  bnj110  31473  bnj1204  31625  bnj1253  31630  connpconn  31762  iscvm  31786  wsuclem  32308  conway  32448  poimirlem28  33980  sstotbnd2  34114  igenval  34401  igenidl  34403  pmap0  35839  pellfundre  38288  pellfundge  38289  pellfundglb  38292  dgraalem  38557  rgspncl  38581  uzwo4  40037  ioodvbdlimc1lem1  40940  fourierdlem31  41148  fourierdlem64  41180  etransclem48  41292  subsaliuncl  41366  smflimlem6  41777  smfpimcc  41807  prmdvdsfmtnof1lem1  42325  prmdvdsfmtnof  42327