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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-dif 3909  df-nul 4287

This theorem is used by:  class2set  5327  reusv2  5376  exss  5446  frminex  5642  weniso  7363  onminesb  7798  onminsb  7799  onminex  7807  oeeulem  8593  supval2  9422  ordtypelem3  9489  card2on  9523  tz9.12lem3  9768  rankf  9773  scott0b  9873  scott0OLD  9874  kardenOLD  9896  cardf2  9945  cardval3  9954  cardmin2  10001  acni3  10047  kmlem3  10152  cofsmo  10268  coftr  10272  fin23lem7  10315  enfin2i  10320  axcc4  10438  axdc3lem4  10452  ac6num  10478  pwfseqlem3  10660  wuncval  10742  wunccl  10744  tskmcl  10841  infm3  12189  nnwos  12955  zsupss  12977  zmin  12984  rpnnen1lem2  13017  rpnnen1lem1  13018  rpnnen1lem3  13019  rpnnen1lem5  13021  ioo0  13413  ico0  13434  ioc0  13435  icc0  13436  bitsfzolem  16514  lcmcllem  16676  fissn0dvdsn0  16700  odzcllem  16874  vdwnn  17080  ram0  17104  ramsey  17112  sylow2blem3  19736  iscyg2  19996  pgpfac1lem5  20195  ablfaclem2  20202  ablfaclem3  20203  ablfac  20204  rgspncl  20762  lspf  21145  ordtrest2lem  23410  ordthauslem  23590  1stcfb  23652  2ndcdisj  23664  ptclsg  23823  txconn  23897  txflf  24214  tsmsfbas  24336  iscmet3  25503  minveclem3b  25638  iundisj  25758  dyadmax  25808  dyadmbllem  25809  elqaalem1  26531  elqaalem3  26533  sgmnncl  27362  musum  27406  conway  28023  incistruhgr  29484  uvtx01vtx  29805  spancl  31759  shsval2i  31810  ococin  31831  iundisjf  33005  iundisjfi  33211  ordtrest2NEWlem  34376  esumrnmpt2  34522  esumpinfval  34527  dmsigagen  34599  ballotlemfc0  34948  ballotlemfcc  34949  ballotlemiex  34957  ballotlemsup  34960  bnj110  35311  bnj1204  35465  bnj1253  35470  connpconn  35764  iscvm  35788  wsuclem  36352  nmuladdel  36741  weiunlem  37031  poimirlem28  38356  sstotbnd2  38483  igenval  38770  igenidl  38772  pmap0  40597  aks4d1p4  42904  aks4d1p5  42905  aks4d1p7  42908  aks4d1p8  42912  grpods  43019  unitscyglem3  43022  unitscyglem4  43023  fsuppind  43380  pellfundre  43666  pellfundge  43667  pellfundglb  43670  dgraalem  43930  uzwo4  45831  ioodvbdlimc1lem1  46703  fourierdlem31  46910  fourierdlem64  46942  etransclem48  47054  subsaliuncl  47130  smflimlem6  47548  smfpimcc  47580  prmdvdsfmtnof1lem1  48394  prmdvdsfmtnof  48396