Theorem rabeq0 4385

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.)

Assertion

Ref	Expression
rabeq0	⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Proof of Theorem rabeq0

Step	Hyp	Ref	Expression
1		ab0 4375	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3431	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2735	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3067	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 302	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 394  ∀wal 1537   = wceq 1539   ∈ wcel 2104  {cab 2707  ∀wral 3059  {crab 3430  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-ral 3060  df-rab 3431  df-dif 3952  df-nul 4324

This theorem is referenced by:  rabn0  4386  rabnc  4388  dffr2ALT  5642  wereu2  5674  frpomin  6342  frpomin2  6343  tz6.26OLD  6350  fndmdifeq0  7046  fnnfpeq0  7179  wemapso2  9552  wemapwe  9696  hashbclem  14417  hashbc  14418  wrdnfi  14504  smuval2  16429  smupvallem  16430  smu01lem  16432  smumullem  16439  phiprmpw  16715  hashgcdeq  16728  prmreclem4  16858  cshws0  17041  pmtrsn  19430  efgsfo  19650  00lsp  20738  dsmm0cl  21516  ordthauslem  23109  pthaus  23364  xkohaus  23379  hmeofval  23484  mumul  26919  musum  26929  ppiub  26941  lgsquadlem2  27118  umgrnloop0  28634  lfgrnloop  28650  numedglnl  28669  usgrnloop0ALT  28727  lfuhgr1v0e  28776  nbuhgr  28865  nbumgr  28869  uhgrnbgr0nb  28876  nbgr0vtxlem  28877  vtxd0nedgb  29010  vtxdusgr0edgnelALT  29018  1loopgrnb0  29024  usgrvd0nedg  29055  vtxdginducedm1lem4  29064  wwlks  29354  iswwlksnon  29372  iswspthsnon  29375  0enwwlksnge1  29383  wspn0  29443  rusgr0edg  29492  clwwlk  29501  clwwlkn  29544  clwwlkn0  29546  clwwlknon  29608  clwwlknon1nloop  29617  clwwlknondisj  29629  vdn0conngrumgrv2  29714  eupth2lemb  29755  eulercrct  29760  frgrregorufr0  29842  numclwwlk3lem2  29902  ofldchr  32700  zarcls1  33145  measvuni  33508  dya2iocuni  33578  repr0  33919  reprlt  33927  reprgt  33929  nummin  34390  subfacp1lem6  34472  prv1n  34718  poimirlem26  36819  poimirlem27  36820  cnambfre  36841  itg2addnclem2  36845  areacirclem5  36885  sticksstones1  41270  nna4b4nsq  41706  0dioph  41820  undisjrab  43369  supminfxr  44474  dvnprodlem3  44964  pimltmnf2f  45713  pimconstlt0  45717  pimgtpnf2f  45721  rmsupp0  47134  lcoc0  47192  rrxsphere  47523