Theorem rabn0 4337

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

Syntax hints:  ¬ wn 3   ↔ wb 208   ≠ wne 3014  ∀wral 3136  ∃wrex 3137  {crab 3140  ∅c0 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-dif 3937  df-nul 4290

This theorem is referenced by:  class2set  5245  reusv2  5294  exss  5346  frminex  5528  weniso  7099  onminesb  7505  onminsb  7506  onminex  7514  oeeulem  8219  supval2  8911  ordtypelem3  8976  card2on  9010  tz9.12lem3  9210  rankf  9215  scott0  9307  karden  9316  cardf2  9364  cardval3  9373  cardmin2  9419  acni3  9465  kmlem3  9570  cofsmo  9683  coftr  9687  fin23lem7  9730  enfin2i  9735  axcc4  9853  axdc3lem4  9867  ac6num  9893  pwfseqlem3  10074  wuncval  10156  wunccl  10158  tskmcl  10255  infm3  11592  nnwos  12307  zsupss  12329  zmin  12336  rpnnen1lem2  12368  rpnnen1lem1  12369  rpnnen1lem3  12370  rpnnen1lem5  12372  ioo0  12755  ico0  12776  ioc0  12777  icc0  12778  bitsfzolem  15775  lcmcllem  15932  fissn0dvdsn0  15956  odzcllem  16121  vdwnn  16326  ram0  16350  ramsey  16358  sylow2blem3  18739  iscyg2  18993  pgpfac1lem5  19193  ablfaclem2  19200  ablfaclem3  19201  ablfac  19202  lspf  19738  ordtrest2lem  21803  ordthauslem  21983  1stcfb  22045  2ndcdisj  22056  ptclsg  22215  txconn  22289  txflf  22606  tsmsfbas  22728  iscmet3  23888  minveclem3b  24023  iundisj  24141  dyadmax  24191  dyadmbllem  24192  elqaalem1  24900  elqaalem3  24902  sgmnncl  25716  musum  25760  incistruhgr  26856  uvtx01vtx  27171  spancl  29105  shsval2i  29156  ococin  29177  iundisjf  30331  iundisjfi  30511  ordtrest2NEWlem  31158  esumrnmpt2  31320  esumpinfval  31325  dmsigagen  31396  ballotlemfc0  31743  ballotlemfcc  31744  ballotlemiex  31752  ballotlemsup  31755  bnj110  32123  bnj1204  32277  bnj1253  32282  connpconn  32475  iscvm  32499  wsuclem  33105  conway  33257  poimirlem28  34912  sstotbnd2  35044  igenval  35331  igenidl  35333  pmap0  36893  pellfundre  39469  pellfundge  39470  pellfundglb  39473  dgraalem  39736  rgspncl  39760  uzwo4  41306  ioodvbdlimc1lem1  42206  fourierdlem31  42414  fourierdlem64  42446  etransclem48  42558  subsaliuncl  42632  smflimlem6  43043  smfpimcc  43073  prmdvdsfmtnof1lem1  43737  prmdvdsfmtnof  43739