Theorem rabeq0 4411

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537   ∈ wcel 2108  {cab 2717  ∀wral 3067  {crab 3443  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-ral 3068  df-rab 3444  df-dif 3979  df-nul 4353

This theorem is referenced by:  rabn0  4412  rabnc  4414  dffr2ALT  5662  wereu2  5697  frpomin  6372  frpomin2  6373  tz6.26OLD  6380  fndmdifeq0  7077  fnnfpeq0  7212  wemapso2  9622  wemapwe  9766  hashbclem  14501  hashbc  14502  wrdnfi  14596  smuval2  16528  smupvallem  16529  smu01lem  16531  smumullem  16538  phiprmpw  16823  hashgcdeq  16836  prmreclem4  16966  cshws0  17149  pmtrsn  19561  efgsfo  19781  00lsp  21002  dsmm0cl  21783  ordthauslem  23412  pthaus  23667  xkohaus  23682  hmeofval  23787  mumul  27242  musum  27252  ppiub  27266  lgsquadlem2  27443  umgrnloop0  29144  lfgrnloop  29160  numedglnl  29179  usgrnloop0ALT  29240  lfuhgr1v0e  29289  nbuhgr  29378  nbumgr  29382  uhgrnbgr0nb  29389  nbgr0edglem  29391  vtxd0nedgb  29524  vtxdusgr0edgnelALT  29532  1loopgrnb0  29538  usgrvd0nedg  29569  vtxdginducedm1lem4  29578  wwlks  29868  iswwlksnon  29886  iswspthsnon  29889  0enwwlksnge1  29897  wspn0  29957  rusgr0edg  30006  clwwlk  30015  clwwlkn  30058  clwwlkn0  30060  clwwlknon  30122  clwwlknon1nloop  30131  clwwlknondisj  30143  vdn0conngrumgrv2  30228  eupth2lemb  30269  eulercrct  30274  frgrregorufr0  30356  numclwwlk3lem2  30416  ofldchr  33309  2sqr3minply  33738  zarcls1  33815  measvuni  34178  dya2iocuni  34248  repr0  34588  reprlt  34596  reprgt  34598  nummin  35067  subfacp1lem6  35153  prv1n  35399  poimirlem26  37606  poimirlem27  37607  cnambfre  37628  itg2addnclem2  37632  areacirclem5  37672  sticksstones1  42103  nna4b4nsq  42615  0dioph  42734  undisjrab  44275  supminfxr  45379  dvnprodlem3  45869  pimltmnf2f  46618  pimconstlt0  46622  pimgtpnf2f  46626  isubgr0uhgr  47743  rmsupp0  48093  lcoc0  48151  rrxsphere  48482