Theorem rabn0 4353

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ≠ wne 2964  ∀wral 3085  ∃wrex 3095  {crab 3423  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-dif 3916  df-nul 4295

This theorem is referenced by:  class2set  5326  reusv2  5375  exss  5445  frminex  5641  weniso  7353  onminesb  7791  onminsb  7792  onminex  7800  oeeulem  8586  supval2  9414  ordtypelem3  9481  card2on  9515  tz9.12lem3  9760  rankf  9765  scott0  9859  karden  9880  cardf2  9928  cardval3  9937  cardmin2  9984  acni3  10030  kmlem3  10135  cofsmo  10252  coftr  10256  fin23lem7  10299  enfin2i  10304  axcc4  10422  axdc3lem4  10436  ac6num  10462  pwfseqlem3  10644  wuncval  10726  wunccl  10728  tskmcl  10825  infm3  12173  nnwos  12938  zsupss  12960  zmin  12967  rpnnen1lem2  13000  rpnnen1lem1  13001  rpnnen1lem3  13002  rpnnen1lem5  13004  ioo0  13396  ico0  13417  ioc0  13418  icc0  13419  bitsfzolem  16491  lcmcllem  16653  fissn0dvdsn0  16677  odzcllem  16851  vdwnn  17057  ram0  17081  ramsey  17089  sylow2blem3  19691  iscyg2  19951  pgpfac1lem5  20150  ablfaclem2  20157  ablfaclem3  20158  ablfac  20159  rgspncl  20697  lspf  21072  ordtrest2lem  23328  ordthauslem  23508  1stcfb  23570  2ndcdisj  23581  ptclsg  23740  txconn  23814  txflf  24131  tsmsfbas  24253  iscmet3  25420  minveclem3b  25555  iundisj  25675  dyadmax  25725  dyadmbllem  25726  elqaalem1  26448  elqaalem3  26450  sgmnncl  27276  musum  27320  conway  27937  incistruhgr  29369  uvtx01vtx  29687  spancl  31628  shsval2i  31679  ococin  31700  iundisjf  32874  iundisjfi  33081  ordtrest2NEWlem  34256  esumrnmpt2  34402  esumpinfval  34407  dmsigagen  34478  ballotlemfc0  34827  ballotlemfcc  34828  ballotlemiex  34836  ballotlemsup  34839  bnj110  35190  bnj1204  35344  bnj1253  35349  connpconn  35625  iscvm  35649  wsuclem  36213  weiunlem  36862  poimirlem28  38186  sstotbnd2  38312  igenval  38599  igenidl  38601  pmap0  40428  aks4d1p4  42735  aks4d1p5  42736  aks4d1p7  42739  aks4d1p8  42743  grpods  42850  unitscyglem3  42853  unitscyglem4  42854  fsuppind  43213  pellfundre  43499  pellfundge  43500  pellfundglb  43503  dgraalem  43763  uzwo4  45664  ioodvbdlimc1lem1  46536  fourierdlem31  46743  fourierdlem64  46775  etransclem48  46887  subsaliuncl  46963  smflimlem6  47381  smfpimcc  47413  prmdvdsfmtnof1lem1  48224  prmdvdsfmtnof  48226