Theorem rabn0 4339

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  {crab 3397  ∅c0 4283

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 2182  ax-ext 2706

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 2713  df-cleq 2726  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-dif 3902  df-nul 4284

This theorem is referenced by:  class2set  5298  reusv2  5346  exss  5409  frminex  5601  weniso  7298  onminesb  7736  onminsb  7737  onminex  7745  oeeulem  8527  supval2  9356  ordtypelem3  9423  card2on  9457  tz9.12lem3  9699  rankf  9704  scott0  9796  karden  9805  cardf2  9853  cardval3  9862  cardmin2  9909  acni3  9955  kmlem3  10061  cofsmo  10177  coftr  10181  fin23lem7  10224  enfin2i  10229  axcc4  10347  axdc3lem4  10361  ac6num  10387  pwfseqlem3  10569  wuncval  10651  wunccl  10653  tskmcl  10750  infm3  12099  nnwos  12826  zsupss  12848  zmin  12855  rpnnen1lem2  12888  rpnnen1lem1  12889  rpnnen1lem3  12890  rpnnen1lem5  12892  ioo0  13284  ico0  13305  ioc0  13306  icc0  13307  bitsfzolem  16359  lcmcllem  16521  fissn0dvdsn0  16545  odzcllem  16718  vdwnn  16924  ram0  16948  ramsey  16956  sylow2blem3  19549  iscyg2  19809  pgpfac1lem5  20008  ablfaclem2  20015  ablfaclem3  20016  ablfac  20017  rgspncl  20544  lspf  20923  ordtrest2lem  23145  ordthauslem  23325  1stcfb  23387  2ndcdisj  23398  ptclsg  23557  txconn  23631  txflf  23948  tsmsfbas  24070  iscmet3  25247  minveclem3b  25382  iundisj  25503  dyadmax  25553  dyadmbllem  25554  elqaalem1  26281  elqaalem3  26283  sgmnncl  27111  musum  27155  conway  27767  incistruhgr  29101  uvtx01vtx  29419  spancl  31360  shsval2i  31411  ococin  31432  iundisjf  32613  iundisjfi  32825  ordtrest2NEWlem  34028  esumrnmpt2  34174  esumpinfval  34179  dmsigagen  34250  ballotlemfc0  34599  ballotlemfcc  34600  ballotlemiex  34608  ballotlemsup  34611  bnj110  34963  bnj1204  35117  bnj1253  35122  connpconn  35378  iscvm  35402  wsuclem  35966  weiunlem2  36606  poimirlem28  37788  sstotbnd2  37914  igenval  38201  igenidl  38203  pmap0  39964  aks4d1p4  42272  aks4d1p5  42273  aks4d1p7  42276  aks4d1p8  42280  grpods  42387  unitscyglem3  42390  unitscyglem4  42391  fsuppind  42775  pellfundre  43065  pellfundge  43066  pellfundglb  43069  dgraalem  43329  uzwo4  45240  ioodvbdlimc1lem1  46117  fourierdlem31  46324  fourierdlem64  46356  etransclem48  46468  subsaliuncl  46544  smflimlem6  46962  smfpimcc  46994  prmdvdsfmtnof1lem1  47772  prmdvdsfmtnof  47774