Theorem rabn0 4343

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ≠ wne 2957  ∀wral 3076  ∃wrex 3086  {crab 3414  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-dif 3907  df-nul 4286

This theorem is referenced by:  class2set  5311  reusv2  5360  exss  5430  frminex  5626  weniso  7338  onminesb  7776  onminsb  7777  onminex  7785  oeeulem  8571  supval2  9401  ordtypelem3  9468  card2on  9502  tz9.12lem3  9747  rankf  9752  scott0  9844  karden  9853  cardf2  9901  cardval3  9910  cardmin2  9957  acni3  10003  kmlem3  10109  cofsmo  10226  coftr  10230  fin23lem7  10273  enfin2i  10278  axcc4  10396  axdc3lem4  10410  ac6num  10436  pwfseqlem3  10618  wuncval  10700  wunccl  10702  tskmcl  10799  infm3  12151  nnwos  12916  zsupss  12938  zmin  12945  rpnnen1lem2  12978  rpnnen1lem1  12979  rpnnen1lem3  12980  rpnnen1lem5  12982  ioo0  13374  ico0  13395  ioc0  13396  icc0  13397  bitsfzolem  16468  lcmcllem  16630  fissn0dvdsn0  16654  odzcllem  16828  vdwnn  17034  ram0  17058  ramsey  17066  sylow2blem3  19662  iscyg2  19922  pgpfac1lem5  20121  ablfaclem2  20128  ablfaclem3  20129  ablfac  20130  rgspncl  20659  lspf  21038  ordtrest2lem  23260  ordthauslem  23440  1stcfb  23502  2ndcdisj  23513  ptclsg  23672  txconn  23746  txflf  24063  tsmsfbas  24185  iscmet3  25352  minveclem3b  25487  iundisj  25607  dyadmax  25657  dyadmbllem  25658  elqaalem1  26380  elqaalem3  26382  sgmnncl  27208  musum  27252  conway  27869  incistruhgr  29277  uvtx01vtx  29595  spancl  31536  shsval2i  31587  ococin  31608  iundisjf  32786  iundisjfi  32995  ordtrest2NEWlem  34216  esumrnmpt2  34362  esumpinfval  34367  dmsigagen  34438  ballotlemfc0  34787  ballotlemfcc  34788  ballotlemiex  34796  ballotlemsup  34799  bnj110  35150  bnj1204  35304  bnj1253  35309  connpconn  35582  iscvm  35606  wsuclem  36170  weiunlem  36820  poimirlem28  38144  sstotbnd2  38270  igenval  38557  igenidl  38559  pmap0  40386  aks4d1p4  42693  aks4d1p5  42694  aks4d1p7  42697  aks4d1p8  42701  grpods  42808  unitscyglem3  42811  unitscyglem4  42812  fsuppind  43169  pellfundre  43455  pellfundge  43456  pellfundglb  43459  dgraalem  43719  uzwo4  45630  ioodvbdlimc1lem1  46502  fourierdlem31  46709  fourierdlem64  46741  etransclem48  46853  subsaliuncl  46929  smflimlem6  47347  smfpimcc  47379  prmdvdsfmtnof1lem1  48190  prmdvdsfmtnof  48192