Theorem rabn0 4350

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3405  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-dif 3916  df-nul 4288

This theorem is referenced by:  class2set  5315  reusv2  5363  exss  5425  frminex  5618  weniso  7304  onminesb  7733  onminsb  7734  onminex  7742  oeeulem  8553  supval2  9400  ordtypelem3  9465  card2on  9499  tz9.12lem3  9734  rankf  9739  scott0  9831  karden  9840  cardf2  9888  cardval3  9897  cardmin2  9944  acni3  9992  kmlem3  10097  cofsmo  10214  coftr  10218  fin23lem7  10261  enfin2i  10266  axcc4  10384  axdc3lem4  10398  ac6num  10424  pwfseqlem3  10605  wuncval  10687  wunccl  10689  tskmcl  10786  infm3  12123  nnwos  12849  zsupss  12871  zmin  12878  rpnnen1lem2  12911  rpnnen1lem1  12912  rpnnen1lem3  12913  rpnnen1lem5  12915  ioo0  13299  ico0  13320  ioc0  13321  icc0  13322  bitsfzolem  16325  lcmcllem  16483  fissn0dvdsn0  16507  odzcllem  16675  vdwnn  16881  ram0  16905  ramsey  16913  sylow2blem3  19418  iscyg2  19673  pgpfac1lem5  19872  ablfaclem2  19879  ablfaclem3  19880  ablfac  19881  lspf  20492  ordtrest2lem  22591  ordthauslem  22771  1stcfb  22833  2ndcdisj  22844  ptclsg  23003  txconn  23077  txflf  23394  tsmsfbas  23516  iscmet3  24694  minveclem3b  24829  iundisj  24949  dyadmax  24999  dyadmbllem  25000  elqaalem1  25716  elqaalem3  25718  sgmnncl  26533  musum  26577  conway  27181  incistruhgr  28093  uvtx01vtx  28408  spancl  30341  shsval2i  30392  ococin  30413  iundisjf  31574  iundisjfi  31767  ordtrest2NEWlem  32592  esumrnmpt2  32756  esumpinfval  32761  dmsigagen  32832  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemiex  33190  ballotlemsup  33193  bnj110  33559  bnj1204  33713  bnj1253  33718  connpconn  33916  iscvm  33940  wsuclem  34486  poimirlem28  36179  sstotbnd2  36306  igenval  36593  igenidl  36595  pmap0  38301  aks4d1p4  40609  aks4d1p5  40610  aks4d1p7  40613  aks4d1p8  40617  fsuppind  40823  pellfundre  41262  pellfundge  41263  pellfundglb  41266  dgraalem  41530  rgspncl  41554  uzwo4  43383  ioodvbdlimc1lem1  44292  fourierdlem31  44499  fourierdlem64  44531  etransclem48  44643  subsaliuncl  44719  smflimlem6  45137  smfpimcc  45169  prmdvdsfmtnof1lem1  45896  prmdvdsfmtnof  45898