Theorem rabn0 4320

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  {crab 3069  ∅c0 4257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2717  df-cleq 2731  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-dif 3891  df-nul 4258

This theorem is referenced by:  class2set  5277  reusv2  5327  exss  5379  frminex  5570  weniso  7234  onminesb  7652  onminsb  7653  onminex  7661  oeeulem  8441  supval2  9223  ordtypelem3  9288  card2on  9322  tz9.12lem3  9556  rankf  9561  scott0  9653  karden  9662  cardf2  9710  cardval3  9719  cardmin2  9766  acni3  9812  kmlem3  9917  cofsmo  10034  coftr  10038  fin23lem7  10081  enfin2i  10086  axcc4  10204  axdc3lem4  10218  ac6num  10244  pwfseqlem3  10425  wuncval  10507  wunccl  10509  tskmcl  10606  infm3  11943  nnwos  12664  zsupss  12686  zmin  12693  rpnnen1lem2  12726  rpnnen1lem1  12727  rpnnen1lem3  12728  rpnnen1lem5  12730  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  bitsfzolem  16150  lcmcllem  16310  fissn0dvdsn0  16334  odzcllem  16502  vdwnn  16708  ram0  16732  ramsey  16740  sylow2blem3  19236  iscyg2  19491  pgpfac1lem5  19691  ablfaclem2  19698  ablfaclem3  19699  ablfac  19700  lspf  20245  ordtrest2lem  22363  ordthauslem  22543  1stcfb  22605  2ndcdisj  22616  ptclsg  22775  txconn  22849  txflf  23166  tsmsfbas  23288  iscmet3  24466  minveclem3b  24601  iundisj  24721  dyadmax  24771  dyadmbllem  24772  elqaalem1  25488  elqaalem3  25490  sgmnncl  26305  musum  26349  incistruhgr  27458  uvtx01vtx  27773  spancl  29707  shsval2i  29758  ococin  29779  iundisjf  30937  iundisjfi  31126  ordtrest2NEWlem  31881  esumrnmpt2  32045  esumpinfval  32050  dmsigagen  32121  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemiex  32477  ballotlemsup  32480  bnj110  32847  bnj1204  33001  bnj1253  33006  connpconn  33206  iscvm  33230  wsuclem  33828  conway  34002  poimirlem28  35814  sstotbnd2  35941  igenval  36228  igenidl  36230  pmap0  37786  aks4d1p4  40094  aks4d1p5  40095  aks4d1p7  40098  aks4d1p8  40102  fsuppind  40286  pellfundre  40710  pellfundge  40711  pellfundglb  40714  dgraalem  40977  rgspncl  41001  uzwo4  42608  ioodvbdlimc1lem1  43479  fourierdlem31  43686  fourierdlem64  43718  etransclem48  43830  subsaliuncl  43904  smflimlem6  44321  smfpimcc  44352  prmdvdsfmtnof1lem1  45047  prmdvdsfmtnof  45049