Theorem rabn0 4329

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  {crab 3389  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-dif 3892  df-nul 4274

This theorem is referenced by:  class2set  5296  reusv2  5345  exss  5415  frminex  5610  weniso  7309  onminesb  7747  onminsb  7748  onminex  7756  oeeulem  8537  supval2  9368  ordtypelem3  9435  card2on  9469  tz9.12lem3  9713  rankf  9718  scott0  9810  karden  9819  cardf2  9867  cardval3  9876  cardmin2  9923  acni3  9969  kmlem3  10075  cofsmo  10191  coftr  10195  fin23lem7  10238  enfin2i  10243  axcc4  10361  axdc3lem4  10375  ac6num  10401  pwfseqlem3  10583  wuncval  10665  wunccl  10667  tskmcl  10764  infm3  12115  nnwos  12865  zsupss  12887  zmin  12894  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  bitsfzolem  16403  lcmcllem  16565  fissn0dvdsn0  16589  odzcllem  16763  vdwnn  16969  ram0  16993  ramsey  17001  sylow2blem3  19597  iscyg2  19857  pgpfac1lem5  20056  ablfaclem2  20063  ablfaclem3  20064  ablfac  20065  rgspncl  20590  lspf  20969  ordtrest2lem  23168  ordthauslem  23348  1stcfb  23410  2ndcdisj  23421  ptclsg  23580  txconn  23654  txflf  23971  tsmsfbas  24093  iscmet3  25260  minveclem3b  25395  iundisj  25515  dyadmax  25565  dyadmbllem  25566  elqaalem1  26285  elqaalem3  26287  sgmnncl  27110  musum  27154  conway  27771  incistruhgr  29148  uvtx01vtx  29466  spancl  31407  shsval2i  31458  ococin  31479  iundisjf  32659  iundisjfi  32869  ordtrest2NEWlem  34066  esumrnmpt2  34212  esumpinfval  34217  dmsigagen  34288  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemiex  34646  ballotlemsup  34649  bnj110  35000  bnj1204  35154  bnj1253  35159  connpconn  35417  iscvm  35441  wsuclem  36005  weiunlem  36645  poimirlem28  37969  sstotbnd2  38095  igenval  38382  igenidl  38384  pmap0  40211  aks4d1p4  42518  aks4d1p5  42519  aks4d1p7  42522  aks4d1p8  42526  grpods  42633  unitscyglem3  42636  unitscyglem4  42637  fsuppind  43023  pellfundre  43309  pellfundge  43310  pellfundglb  43313  dgraalem  43573  uzwo4  45484  ioodvbdlimc1lem1  46359  fourierdlem31  46566  fourierdlem64  46598  etransclem48  46710  subsaliuncl  46786  smflimlem6  47204  smfpimcc  47236  prmdvdsfmtnof1lem1  48047  prmdvdsfmtnof  48049