Theorem rabn0 4346

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  {crab 3416  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-dif 3908  df-nul 4287

This theorem is referenced by:  class2set  5325  reusv2  5374  exss  5444  frminex  5640  weniso  7352  onminesb  7788  onminsb  7789  onminex  7797  oeeulem  8583  supval2  9411  ordtypelem3  9478  card2on  9512  tz9.12lem3  9757  rankf  9762  scott0  9856  karden  9877  cardf2  9925  cardval3  9934  cardmin2  9981  acni3  10027  kmlem3  10132  cofsmo  10248  coftr  10252  fin23lem7  10295  enfin2i  10300  axcc4  10418  axdc3lem4  10432  ac6num  10458  pwfseqlem3  10640  wuncval  10722  wunccl  10724  tskmcl  10821  infm3  12169  nnwos  12934  zsupss  12956  zmin  12963  rpnnen1lem2  12996  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  bitsfzolem  16487  lcmcllem  16649  fissn0dvdsn0  16673  odzcllem  16847  vdwnn  17053  ram0  17077  ramsey  17085  sylow2blem3  19687  iscyg2  19947  pgpfac1lem5  20146  ablfaclem2  20153  ablfaclem3  20154  ablfac  20155  rgspncl  20712  lspf  21095  ordtrest2lem  23360  ordthauslem  23540  1stcfb  23602  2ndcdisj  23613  ptclsg  23772  txconn  23846  txflf  24163  tsmsfbas  24285  iscmet3  25452  minveclem3b  25587  iundisj  25707  dyadmax  25757  dyadmbllem  25758  elqaalem1  26480  elqaalem3  26482  sgmnncl  27311  musum  27355  conway  27972  incistruhgr  29429  uvtx01vtx  29747  spancl  31688  shsval2i  31739  ococin  31760  iundisjf  32934  iundisjfi  33141  ordtrest2NEWlem  34312  esumrnmpt2  34458  esumpinfval  34463  dmsigagen  34534  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemiex  34892  ballotlemsup  34895  bnj110  35246  bnj1204  35400  bnj1253  35405  connpconn  35727  iscvm  35751  wsuclem  36315  nmuladdel  36689  weiunlem  36974  poimirlem28  38299  sstotbnd2  38425  igenval  38712  igenidl  38714  pmap0  40539  aks4d1p4  42846  aks4d1p5  42847  aks4d1p7  42850  aks4d1p8  42854  grpods  42961  unitscyglem3  42964  unitscyglem4  42965  fsuppind  43322  pellfundre  43608  pellfundge  43609  pellfundglb  43612  dgraalem  43872  uzwo4  45773  ioodvbdlimc1lem1  46645  fourierdlem31  46852  fourierdlem64  46884  etransclem48  46996  subsaliuncl  47072  smflimlem6  47490  smfpimcc  47522  prmdvdsfmtnof1lem1  48336  prmdvdsfmtnof  48338