Theorem rabn0 3958

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

Syntax hints:  ¬ wn 3   ↔ wb 196   ≠ wne 2794  ∀wral 2912  ∃wrex 2913  {crab 2916  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-nul 3916

This theorem is referenced by:  class2set  4832  reusv2  4874  exss  4931  frminex  5094  weniso  6604  onminesb  6998  onminsb  6999  onminex  7007  oeeulem  7681  supval2  8361  ordtypelem3  8425  card2on  8459  tz9.12lem3  8652  rankf  8657  scott0  8749  karden  8758  cardf2  8769  cardval3  8778  cardmin2  8824  acni3  8870  kmlem3  8974  cofsmo  9091  coftr  9095  fin23lem7  9138  enfin2i  9143  axcc4  9261  axdc3lem4  9275  ac6num  9301  pwfseqlem3  9482  wuncval  9564  wunccl  9566  tskmcl  9663  infm3  10982  nnwos  11755  zsupss  11777  zmin  11784  rpnnen1lem2  11814  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  bitsfzolem  15156  lcmcllem  15309  fissn0dvdsn0  15333  odzcllem  15497  vdwnn  15702  ram0  15726  ramsey  15734  sylow2blem3  18037  iscyg2  18284  pgpfac1lem5  18478  ablfaclem2  18485  ablfaclem3  18486  ablfac  18487  lspf  18974  ordtrest2lem  21007  ordthauslem  21187  1stcfb  21248  2ndcdisj  21259  ptclsg  21418  txconn  21492  txflf  21810  tsmsfbas  21931  iscmet3  23091  minveclem3b  23199  iundisj  23316  dyadmax  23366  dyadmbllem  23367  elqaalem1  24074  elqaalem3  24076  sgmnncl  24873  musum  24917  incistruhgr  25974  uvtxa01vtx0  26297  spancl  28195  shsval2i  28246  ococin  28267  iundisjf  29402  iundisjfi  29555  ordtrest2NEWlem  29968  esumrnmpt2  30130  esumpinfval  30135  dmsigagen  30207  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemiex  30563  ballotlemsup  30566  bnj110  30928  bnj1204  31080  bnj1253  31085  connpconn  31217  iscvm  31241  wsuclem  31773  wsuclemOLD  31774  conway  31910  poimirlem28  33437  sstotbnd2  33573  igenval  33860  igenidl  33862  pmap0  35051  pellfundre  37445  pellfundge  37446  pellfundglb  37449  dgraalem  37715  rgspncl  37739  uzwo4  39221  ioodvbdlimc1lem1  40146  fourierdlem31  40355  fourierdlem64  40387  etransclem48  40499  subsaliuncl  40576  smflimlem6  40984  smfpimcc  41014  prmdvdsfmtnof1lem1  41496  prmdvdsfmtnof  41498