Theorem rabn0 4352

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 4351	. . 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 3405  ∅c0 4296

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 3406  df-dif 3917  df-nul 4297

This theorem is referenced by:  class2set  5310  reusv2  5358  exss  5423  frminex  5617  weniso  7329  onminesb  7769  onminsb  7770  onminex  7778  oeeulem  8565  supval2  9406  ordtypelem3  9473  card2on  9507  tz9.12lem3  9742  rankf  9747  scott0  9839  karden  9848  cardf2  9896  cardval3  9905  cardmin2  9952  acni3  10000  kmlem3  10106  cofsmo  10222  coftr  10226  fin23lem7  10269  enfin2i  10274  axcc4  10392  axdc3lem4  10406  ac6num  10432  pwfseqlem3  10613  wuncval  10695  wunccl  10697  tskmcl  10794  infm3  12142  nnwos  12874  zsupss  12896  zmin  12903  rpnnen1lem2  12936  rpnnen1lem1  12937  rpnnen1lem3  12938  rpnnen1lem5  12940  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  bitsfzolem  16404  lcmcllem  16566  fissn0dvdsn0  16590  odzcllem  16763  vdwnn  16969  ram0  16993  ramsey  17001  sylow2blem3  19552  iscyg2  19812  pgpfac1lem5  20011  ablfaclem2  20018  ablfaclem3  20019  ablfac  20020  rgspncl  20522  lspf  20880  ordtrest2lem  23090  ordthauslem  23270  1stcfb  23332  2ndcdisj  23343  ptclsg  23502  txconn  23576  txflf  23893  tsmsfbas  24015  iscmet3  25193  minveclem3b  25328  iundisj  25449  dyadmax  25499  dyadmbllem  25500  elqaalem1  26227  elqaalem3  26229  sgmnncl  27057  musum  27101  conway  27711  incistruhgr  29006  uvtx01vtx  29324  spancl  31265  shsval2i  31316  ococin  31337  iundisjf  32518  iundisjfi  32719  ordtrest2NEWlem  33912  esumrnmpt2  34058  esumpinfval  34063  dmsigagen  34134  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemiex  34493  ballotlemsup  34496  bnj110  34848  bnj1204  35002  bnj1253  35007  connpconn  35222  iscvm  35246  wsuclem  35813  weiunlem2  36451  poimirlem28  37642  sstotbnd2  37768  igenval  38055  igenidl  38057  pmap0  39759  aks4d1p4  42067  aks4d1p5  42068  aks4d1p7  42071  aks4d1p8  42075  grpods  42182  unitscyglem3  42185  unitscyglem4  42186  fsuppind  42578  pellfundre  42869  pellfundge  42870  pellfundglb  42873  dgraalem  43134  uzwo4  45047  ioodvbdlimc1lem1  45929  fourierdlem31  46136  fourierdlem64  46168  etransclem48  46280  subsaliuncl  46356  smflimlem6  46774  smfpimcc  46806  prmdvdsfmtnof1lem1  47585  prmdvdsfmtnof  47587