Theorem rabeq0 4368

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2714  ∀wral 3052  {crab 3420  ∅c0 4313

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 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

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 2066  df-clab 2715  df-cleq 2728  df-ral 3053  df-rab 3421  df-dif 3934  df-nul 4314

This theorem is referenced by:  rabn0  4369  rabnc  4371  dffr2ALT  5621  wereu2  5656  frpomin  6334  frpomin2  6335  tz6.26OLD  6342  fndmdifeq0  7039  fnnfpeq0  7175  wemapso2  9572  wemapwe  9716  hashbclem  14475  hashbc  14476  wrdnfi  14571  smuval2  16506  smupvallem  16507  smu01lem  16509  smumullem  16516  phiprmpw  16800  hashgcdeq  16814  prmreclem4  16944  cshws0  17126  pmtrsn  19505  efgsfo  19725  00lsp  20943  dsmm0cl  21705  ordthauslem  23326  pthaus  23581  xkohaus  23596  hmeofval  23701  mumul  27148  musum  27158  ppiub  27172  lgsquadlem2  27349  umgrnloop0  29093  lfgrnloop  29109  numedglnl  29128  usgrnloop0ALT  29189  lfuhgr1v0e  29238  nbuhgr  29327  nbumgr  29331  uhgrnbgr0nb  29338  nbgr0edglem  29340  vtxd0nedgb  29473  vtxdusgr0edgnelALT  29481  1loopgrnb0  29487  usgrvd0nedg  29518  vtxdginducedm1lem4  29527  wwlks  29822  iswwlksnon  29840  iswspthsnon  29843  0enwwlksnge1  29851  wspn0  29911  rusgr0edg  29960  clwwlk  29969  clwwlkn  30012  clwwlkn0  30014  clwwlknon  30076  clwwlknon1nloop  30085  clwwlknondisj  30097  vdn0conngrumgrv2  30182  eupth2lemb  30223  eulercrct  30228  frgrregorufr0  30310  numclwwlk3lem2  30370  ofldchr  33341  2sqr3minply  33819  cos9thpiminply  33827  zarcls1  33905  measvuni  34250  dya2iocuni  34320  repr0  34648  reprlt  34656  reprgt  34658  nummin  35127  subfacp1lem6  35212  prv1n  35458  poimirlem26  37675  poimirlem27  37676  cnambfre  37697  itg2addnclem2  37701  areacirclem5  37741  sticksstones1  42164  nna4b4nsq  42658  0dioph  42776  undisjrab  44305  supminfxr  45471  dvnprodlem3  45957  pimltmnf2f  46706  pimconstlt0  46710  pimgtpnf2f  46714  isubgr0uhgr  47866  stgr0  47952  rmsupp0  48323  lcoc0  48378  rrxsphere  48708