Theorem rabn0 4348

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 4347	. . 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 3402  ∅c0 4292

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 3403  df-dif 3914  df-nul 4293

This theorem is referenced by:  class2set  5305  reusv2  5353  exss  5418  frminex  5610  weniso  7311  onminesb  7749  onminsb  7750  onminex  7758  oeeulem  8542  supval2  9382  ordtypelem3  9449  card2on  9483  tz9.12lem3  9718  rankf  9723  scott0  9815  karden  9824  cardf2  9872  cardval3  9881  cardmin2  9928  acni3  9976  kmlem3  10082  cofsmo  10198  coftr  10202  fin23lem7  10245  enfin2i  10250  axcc4  10368  axdc3lem4  10382  ac6num  10408  pwfseqlem3  10589  wuncval  10671  wunccl  10673  tskmcl  10770  infm3  12118  nnwos  12850  zsupss  12872  zmin  12879  rpnnen1lem2  12912  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  ioo0  13307  ico0  13328  ioc0  13329  icc0  13330  bitsfzolem  16380  lcmcllem  16542  fissn0dvdsn0  16566  odzcllem  16739  vdwnn  16945  ram0  16969  ramsey  16977  sylow2blem3  19528  iscyg2  19788  pgpfac1lem5  19987  ablfaclem2  19994  ablfaclem3  19995  ablfac  19996  rgspncl  20498  lspf  20856  ordtrest2lem  23066  ordthauslem  23246  1stcfb  23308  2ndcdisj  23319  ptclsg  23478  txconn  23552  txflf  23869  tsmsfbas  23991  iscmet3  25169  minveclem3b  25304  iundisj  25425  dyadmax  25475  dyadmbllem  25476  elqaalem1  26203  elqaalem3  26205  sgmnncl  27033  musum  27077  conway  27687  incistruhgr  28982  uvtx01vtx  29300  spancl  31238  shsval2i  31289  ococin  31310  iundisjf  32491  iundisjfi  32692  ordtrest2NEWlem  33885  esumrnmpt2  34031  esumpinfval  34036  dmsigagen  34107  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemsup  34469  bnj110  34821  bnj1204  34975  bnj1253  34980  connpconn  35195  iscvm  35219  wsuclem  35786  weiunlem2  36424  poimirlem28  37615  sstotbnd2  37741  igenval  38028  igenidl  38030  pmap0  39732  aks4d1p4  42040  aks4d1p5  42041  aks4d1p7  42044  aks4d1p8  42048  grpods  42155  unitscyglem3  42158  unitscyglem4  42159  fsuppind  42551  pellfundre  42842  pellfundge  42843  pellfundglb  42846  dgraalem  43107  uzwo4  45020  ioodvbdlimc1lem1  45902  fourierdlem31  46109  fourierdlem64  46141  etransclem48  46253  subsaliuncl  46329  smflimlem6  46747  smfpimcc  46779  prmdvdsfmtnof1lem1  47558  prmdvdsfmtnof  47560