Theorem rabn0 4369

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-dif 3934  df-nul 4314

This theorem is referenced by:  class2set  5330  reusv2  5378  exss  5443  frminex  5638  weniso  7352  onminesb  7792  onminsb  7793  onminex  7801  oeeulem  8618  supval2  9472  ordtypelem3  9539  card2on  9573  tz9.12lem3  9808  rankf  9813  scott0  9905  karden  9914  cardf2  9962  cardval3  9971  cardmin2  10018  acni3  10066  kmlem3  10172  cofsmo  10288  coftr  10292  fin23lem7  10335  enfin2i  10340  axcc4  10458  axdc3lem4  10472  ac6num  10498  pwfseqlem3  10679  wuncval  10761  wunccl  10763  tskmcl  10860  infm3  12206  nnwos  12936  zsupss  12958  zmin  12965  rpnnen1lem2  12998  rpnnen1lem1  12999  rpnnen1lem3  13000  rpnnen1lem5  13002  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  bitsfzolem  16458  lcmcllem  16620  fissn0dvdsn0  16644  odzcllem  16817  vdwnn  17023  ram0  17047  ramsey  17055  sylow2blem3  19608  iscyg2  19868  pgpfac1lem5  20067  ablfaclem2  20074  ablfaclem3  20075  ablfac  20076  rgspncl  20578  lspf  20936  ordtrest2lem  23146  ordthauslem  23326  1stcfb  23388  2ndcdisj  23399  ptclsg  23558  txconn  23632  txflf  23949  tsmsfbas  24071  iscmet3  25250  minveclem3b  25385  iundisj  25506  dyadmax  25556  dyadmbllem  25557  elqaalem1  26284  elqaalem3  26286  sgmnncl  27114  musum  27158  conway  27768  incistruhgr  29063  uvtx01vtx  29381  spancl  31322  shsval2i  31373  ococin  31394  iundisjf  32575  iundisjfi  32778  ordtrest2NEWlem  33958  esumrnmpt2  34104  esumpinfval  34109  dmsigagen  34180  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemiex  34539  ballotlemsup  34542  bnj110  34894  bnj1204  35048  bnj1253  35053  connpconn  35262  iscvm  35286  wsuclem  35848  weiunlem2  36486  poimirlem28  37677  sstotbnd2  37803  igenval  38090  igenidl  38092  pmap0  39789  aks4d1p4  42097  aks4d1p5  42098  aks4d1p7  42101  aks4d1p8  42105  grpods  42212  unitscyglem3  42215  unitscyglem4  42216  fsuppind  42588  pellfundre  42879  pellfundge  42880  pellfundglb  42883  dgraalem  43144  uzwo4  45057  ioodvbdlimc1lem1  45940  fourierdlem31  46147  fourierdlem64  46179  etransclem48  46291  subsaliuncl  46367  smflimlem6  46785  smfpimcc  46817  prmdvdsfmtnof1lem1  47578  prmdvdsfmtnof  47580