Theorem rabeq0 4347

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2707  ∀wral 3044  {crab 3402  ∅c0 4292

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 2701

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 2708  df-cleq 2721  df-ral 3045  df-rab 3403  df-dif 3914  df-nul 4293

This theorem is referenced by:  rabn0  4348  rabnc  4350  dffr2ALT  5593  wereu2  5628  frpomin  6301  frpomin2  6302  fndmdifeq0  6998  fnnfpeq0  7134  wemapso2  9482  wemapwe  9626  hashbclem  14393  hashbc  14394  wrdnfi  14489  smuval2  16428  smupvallem  16429  smu01lem  16431  smumullem  16438  phiprmpw  16722  hashgcdeq  16736  prmreclem4  16866  cshws0  17048  pmtrsn  19425  efgsfo  19645  00lsp  20863  dsmm0cl  21625  ordthauslem  23246  pthaus  23501  xkohaus  23516  hmeofval  23621  mumul  27067  musum  27077  ppiub  27091  lgsquadlem2  27268  umgrnloop0  29012  lfgrnloop  29028  numedglnl  29047  usgrnloop0ALT  29108  lfuhgr1v0e  29157  nbuhgr  29246  nbumgr  29250  uhgrnbgr0nb  29257  nbgr0edglem  29259  vtxd0nedgb  29392  vtxdusgr0edgnelALT  29400  1loopgrnb0  29406  usgrvd0nedg  29437  vtxdginducedm1lem4  29446  wwlks  29738  iswwlksnon  29756  iswspthsnon  29759  0enwwlksnge1  29767  wspn0  29827  rusgr0edg  29876  clwwlk  29885  clwwlkn  29928  clwwlkn0  29930  clwwlknon  29992  clwwlknon1nloop  30001  clwwlknondisj  30013  vdn0conngrumgrv2  30098  eupth2lemb  30139  eulercrct  30144  frgrregorufr0  30226  numclwwlk3lem2  30286  ofldchr  33265  2sqr3minply  33743  cos9thpiminply  33751  zarcls1  33832  measvuni  34177  dya2iocuni  34247  repr0  34575  reprlt  34583  reprgt  34585  nummin  35054  subfacp1lem6  35145  prv1n  35391  poimirlem26  37613  poimirlem27  37614  cnambfre  37635  itg2addnclem2  37639  areacirclem5  37679  sticksstones1  42107  nna4b4nsq  42621  0dioph  42739  undisjrab  44268  supminfxr  45433  dvnprodlem3  45919  pimltmnf2f  46668  pimconstlt0  46672  pimgtpnf2f  46676  isubgr0uhgr  47846  stgr0  47932  rmsupp0  48329  lcoc0  48384  rrxsphere  48710