Theorem rabn0 4340

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  {crab 3394  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-dif 3906  df-nul 4285

This theorem is referenced by:  class2set  5294  reusv2  5342  exss  5406  frminex  5598  weniso  7291  onminesb  7729  onminsb  7730  onminex  7738  oeeulem  8519  supval2  9345  ordtypelem3  9412  card2on  9446  tz9.12lem3  9685  rankf  9690  scott0  9782  karden  9791  cardf2  9839  cardval3  9848  cardmin2  9895  acni3  9941  kmlem3  10047  cofsmo  10163  coftr  10167  fin23lem7  10210  enfin2i  10215  axcc4  10333  axdc3lem4  10347  ac6num  10373  pwfseqlem3  10554  wuncval  10636  wunccl  10638  tskmcl  10735  infm3  12084  nnwos  12816  zsupss  12838  zmin  12845  rpnnen1lem2  12878  rpnnen1lem1  12879  rpnnen1lem3  12880  rpnnen1lem5  12882  ioo0  13273  ico0  13294  ioc0  13295  icc0  13296  bitsfzolem  16345  lcmcllem  16507  fissn0dvdsn0  16531  odzcllem  16704  vdwnn  16910  ram0  16934  ramsey  16942  sylow2blem3  19501  iscyg2  19761  pgpfac1lem5  19960  ablfaclem2  19967  ablfaclem3  19968  ablfac  19969  rgspncl  20498  lspf  20877  ordtrest2lem  23088  ordthauslem  23268  1stcfb  23330  2ndcdisj  23341  ptclsg  23500  txconn  23574  txflf  23891  tsmsfbas  24013  iscmet3  25191  minveclem3b  25326  iundisj  25447  dyadmax  25497  dyadmbllem  25498  elqaalem1  26225  elqaalem3  26227  sgmnncl  27055  musum  27099  conway  27710  incistruhgr  29024  uvtx01vtx  29342  spancl  31280  shsval2i  31331  ococin  31352  iundisjf  32533  iundisjfi  32739  ordtrest2NEWlem  33889  esumrnmpt2  34035  esumpinfval  34040  dmsigagen  34111  ballotlemfc0  34461  ballotlemfcc  34462  ballotlemiex  34470  ballotlemsup  34473  bnj110  34825  bnj1204  34979  bnj1253  34984  connpconn  35208  iscvm  35232  wsuclem  35799  weiunlem2  36437  poimirlem28  37628  sstotbnd2  37754  igenval  38041  igenidl  38043  pmap0  39744  aks4d1p4  42052  aks4d1p5  42053  aks4d1p7  42056  aks4d1p8  42060  grpods  42167  unitscyglem3  42170  unitscyglem4  42171  fsuppind  42563  pellfundre  42854  pellfundge  42855  pellfundglb  42858  dgraalem  43118  uzwo4  45031  ioodvbdlimc1lem1  45912  fourierdlem31  46119  fourierdlem64  46151  etransclem48  46263  subsaliuncl  46339  smflimlem6  46757  smfpimcc  46789  prmdvdsfmtnof1lem1  47568  prmdvdsfmtnof  47570