Theorem rabeq0 4363

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 4355	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3416	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2740	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3059	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 303	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2108  {cab 2713  ∀wral 3051  {crab 3415  ∅c0 4308

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-ral 3052  df-rab 3416  df-dif 3929  df-nul 4309

This theorem is referenced by:  rabn0  4364  rabnc  4366  dffr2ALT  5616  wereu2  5651  frpomin  6329  frpomin2  6330  tz6.26OLD  6337  fndmdifeq0  7033  fnnfpeq0  7169  wemapso2  9565  wemapwe  9709  hashbclem  14468  hashbc  14469  wrdnfi  14564  smuval2  16499  smupvallem  16500  smu01lem  16502  smumullem  16509  phiprmpw  16793  hashgcdeq  16807  prmreclem4  16937  cshws0  17119  pmtrsn  19498  efgsfo  19718  00lsp  20936  dsmm0cl  21698  ordthauslem  23319  pthaus  23574  xkohaus  23589  hmeofval  23694  mumul  27141  musum  27151  ppiub  27165  lgsquadlem2  27342  umgrnloop0  29034  lfgrnloop  29050  numedglnl  29069  usgrnloop0ALT  29130  lfuhgr1v0e  29179  nbuhgr  29268  nbumgr  29272  uhgrnbgr0nb  29279  nbgr0edglem  29281  vtxd0nedgb  29414  vtxdusgr0edgnelALT  29422  1loopgrnb0  29428  usgrvd0nedg  29459  vtxdginducedm1lem4  29468  wwlks  29763  iswwlksnon  29781  iswspthsnon  29784  0enwwlksnge1  29792  wspn0  29852  rusgr0edg  29901  clwwlk  29910  clwwlkn  29953  clwwlkn0  29955  clwwlknon  30017  clwwlknon1nloop  30026  clwwlknondisj  30038  vdn0conngrumgrv2  30123  eupth2lemb  30164  eulercrct  30169  frgrregorufr0  30251  numclwwlk3lem2  30311  ofldchr  33282  2sqr3minply  33760  cos9thpiminply  33768  zarcls1  33846  measvuni  34191  dya2iocuni  34261  repr0  34589  reprlt  34597  reprgt  34599  nummin  35068  subfacp1lem6  35153  prv1n  35399  poimirlem26  37616  poimirlem27  37617  cnambfre  37638  itg2addnclem2  37642  areacirclem5  37682  sticksstones1  42105  nna4b4nsq  42630  0dioph  42748  undisjrab  44278  supminfxr  45439  dvnprodlem3  45925  pimltmnf2f  46674  pimconstlt0  46678  pimgtpnf2f  46682  isubgr0uhgr  47834  stgr0  47920  rmsupp0  48291  lcoc0  48346  rrxsphere  48676