Theorem rabn0 4341

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  {crab 3399  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-dif 3904  df-nul 4286

This theorem is referenced by:  class2set  5300  reusv2  5348  exss  5411  frminex  5603  weniso  7300  onminesb  7738  onminsb  7739  onminex  7747  oeeulem  8529  supval2  9358  ordtypelem3  9425  card2on  9459  tz9.12lem3  9701  rankf  9706  scott0  9798  karden  9807  cardf2  9855  cardval3  9864  cardmin2  9911  acni3  9957  kmlem3  10063  cofsmo  10179  coftr  10183  fin23lem7  10226  enfin2i  10231  axcc4  10349  axdc3lem4  10363  ac6num  10389  pwfseqlem3  10571  wuncval  10653  wunccl  10655  tskmcl  10752  infm3  12101  nnwos  12828  zsupss  12850  zmin  12857  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  ioo0  13286  ico0  13307  ioc0  13308  icc0  13309  bitsfzolem  16361  lcmcllem  16523  fissn0dvdsn0  16547  odzcllem  16720  vdwnn  16926  ram0  16950  ramsey  16958  sylow2blem3  19551  iscyg2  19811  pgpfac1lem5  20010  ablfaclem2  20017  ablfaclem3  20018  ablfac  20019  rgspncl  20546  lspf  20925  ordtrest2lem  23147  ordthauslem  23327  1stcfb  23389  2ndcdisj  23400  ptclsg  23559  txconn  23633  txflf  23950  tsmsfbas  24072  iscmet3  25249  minveclem3b  25384  iundisj  25505  dyadmax  25555  dyadmbllem  25556  elqaalem1  26283  elqaalem3  26285  sgmnncl  27113  musum  27157  conway  27775  incistruhgr  29152  uvtx01vtx  29470  spancl  31411  shsval2i  31462  ococin  31483  iundisjf  32664  iundisjfi  32876  ordtrest2NEWlem  34079  esumrnmpt2  34225  esumpinfval  34230  dmsigagen  34301  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemiex  34659  ballotlemsup  34662  bnj110  35014  bnj1204  35168  bnj1253  35173  connpconn  35429  iscvm  35453  wsuclem  36017  weiunlem  36657  poimirlem28  37849  sstotbnd2  37975  igenval  38262  igenidl  38264  pmap0  40025  aks4d1p4  42333  aks4d1p5  42334  aks4d1p7  42337  aks4d1p8  42341  grpods  42448  unitscyglem3  42451  unitscyglem4  42452  fsuppind  42833  pellfundre  43123  pellfundge  43124  pellfundglb  43127  dgraalem  43387  uzwo4  45298  ioodvbdlimc1lem1  46175  fourierdlem31  46382  fourierdlem64  46414  etransclem48  46526  subsaliuncl  46602  smflimlem6  47020  smfpimcc  47052  prmdvdsfmtnof1lem1  47830  prmdvdsfmtnof  47832