Theorem rabn0 4336

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395  ∅c0 4280

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 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2710  df-cleq 2723  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-dif 3900  df-nul 4281

This theorem is referenced by:  class2set  5291  reusv2  5339  exss  5401  frminex  5593  weniso  7288  onminesb  7726  onminsb  7727  onminex  7735  oeeulem  8516  supval2  9339  ordtypelem3  9406  card2on  9440  tz9.12lem3  9682  rankf  9687  scott0  9779  karden  9788  cardf2  9836  cardval3  9845  cardmin2  9892  acni3  9938  kmlem3  10044  cofsmo  10160  coftr  10164  fin23lem7  10207  enfin2i  10212  axcc4  10330  axdc3lem4  10344  ac6num  10370  pwfseqlem3  10551  wuncval  10633  wunccl  10635  tskmcl  10732  infm3  12081  nnwos  12813  zsupss  12835  zmin  12842  rpnnen1lem2  12875  rpnnen1lem1  12876  rpnnen1lem3  12877  rpnnen1lem5  12879  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  bitsfzolem  16345  lcmcllem  16507  fissn0dvdsn0  16531  odzcllem  16704  vdwnn  16910  ram0  16934  ramsey  16942  sylow2blem3  19534  iscyg2  19794  pgpfac1lem5  19993  ablfaclem2  20000  ablfaclem3  20001  ablfac  20002  rgspncl  20528  lspf  20907  ordtrest2lem  23118  ordthauslem  23298  1stcfb  23360  2ndcdisj  23371  ptclsg  23530  txconn  23604  txflf  23921  tsmsfbas  24043  iscmet3  25220  minveclem3b  25355  iundisj  25476  dyadmax  25526  dyadmbllem  25527  elqaalem1  26254  elqaalem3  26256  sgmnncl  27084  musum  27128  conway  27740  incistruhgr  29057  uvtx01vtx  29375  spancl  31316  shsval2i  31367  ococin  31388  iundisjf  32569  iundisjfi  32778  ordtrest2NEWlem  33935  esumrnmpt2  34081  esumpinfval  34086  dmsigagen  34157  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemiex  34515  ballotlemsup  34518  bnj110  34870  bnj1204  35024  bnj1253  35029  connpconn  35279  iscvm  35303  wsuclem  35867  weiunlem2  36505  poimirlem28  37696  sstotbnd2  37822  igenval  38109  igenidl  38111  pmap0  39812  aks4d1p4  42120  aks4d1p5  42121  aks4d1p7  42124  aks4d1p8  42128  grpods  42235  unitscyglem3  42238  unitscyglem4  42239  fsuppind  42631  pellfundre  42922  pellfundge  42923  pellfundglb  42926  dgraalem  43186  uzwo4  45098  ioodvbdlimc1lem1  45977  fourierdlem31  46184  fourierdlem64  46216  etransclem48  46328  subsaliuncl  46404  smflimlem6  46822  smfpimcc  46854  prmdvdsfmtnof1lem1  47623  prmdvdsfmtnof  47625