Theorem rabn0 4388

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2939  ∀wral 3060  ∃wrex 3069  {crab 3435  ∅c0 4332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-clab 2714  df-cleq 2728  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-dif 3953  df-nul 4333

This theorem is referenced by:  class2set  5354  reusv2  5402  exss  5467  frminex  5663  weniso  7375  onminesb  7814  onminsb  7815  onminex  7823  oeeulem  8640  supval2  9496  ordtypelem3  9561  card2on  9595  tz9.12lem3  9830  rankf  9835  scott0  9927  karden  9936  cardf2  9984  cardval3  9993  cardmin2  10040  acni3  10088  kmlem3  10194  cofsmo  10310  coftr  10314  fin23lem7  10357  enfin2i  10362  axcc4  10480  axdc3lem4  10494  ac6num  10520  pwfseqlem3  10701  wuncval  10783  wunccl  10785  tskmcl  10882  infm3  12228  nnwos  12958  zsupss  12980  zmin  12987  rpnnen1lem2  13020  rpnnen1lem1  13021  rpnnen1lem3  13022  rpnnen1lem5  13024  ioo0  13413  ico0  13434  ioc0  13435  icc0  13436  bitsfzolem  16472  lcmcllem  16634  fissn0dvdsn0  16658  odzcllem  16831  vdwnn  17037  ram0  17061  ramsey  17069  sylow2blem3  19641  iscyg2  19901  pgpfac1lem5  20100  ablfaclem2  20107  ablfaclem3  20108  ablfac  20109  rgspncl  20614  lspf  20973  ordtrest2lem  23212  ordthauslem  23392  1stcfb  23454  2ndcdisj  23465  ptclsg  23624  txconn  23698  txflf  24015  tsmsfbas  24137  iscmet3  25328  minveclem3b  25463  iundisj  25584  dyadmax  25634  dyadmbllem  25635  elqaalem1  26362  elqaalem3  26364  sgmnncl  27191  musum  27235  conway  27845  incistruhgr  29097  uvtx01vtx  29415  spancl  31356  shsval2i  31407  ococin  31428  iundisjf  32603  iundisjfi  32799  ordtrest2NEWlem  33922  esumrnmpt2  34070  esumpinfval  34075  dmsigagen  34146  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemiex  34505  ballotlemsup  34508  bnj110  34873  bnj1204  35027  bnj1253  35032  connpconn  35241  iscvm  35265  wsuclem  35827  weiunlem2  36465  poimirlem28  37656  sstotbnd2  37782  igenval  38069  igenidl  38071  pmap0  39768  aks4d1p4  42081  aks4d1p5  42082  aks4d1p7  42085  aks4d1p8  42089  grpods  42196  unitscyglem3  42199  unitscyglem4  42200  fsuppind  42605  pellfundre  42897  pellfundge  42898  pellfundglb  42901  dgraalem  43162  uzwo4  45063  ioodvbdlimc1lem1  45951  fourierdlem31  46158  fourierdlem64  46190  etransclem48  46302  subsaliuncl  46378  smflimlem6  46796  smfpimcc  46828  prmdvdsfmtnof1lem1  47576  prmdvdsfmtnof  47578