Theorem rabeq0 4065

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 4059	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3023	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2729	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3093	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 292	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 383  ∀wal 1594   = wceq 1596   ∈ wcel 2103  {cab 2710  ∀wral 3014  {crab 3018  ∅c0 4023

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rab 3023  df-v 3306  df-dif 3683  df-nul 4024

This theorem is referenced by:  rabn0  4066  rabnc  4070  dffr2  5183  frc  5184  frirr  5195  wereu2  5215  tz6.26  5824  fndmdifeq0  6438  fnnfpeq0  6560  wemapso2  8574  wemapwe  8707  hashbclem  13349  hashbc  13350  smuval2  15327  smupvallem  15328  smu01lem  15330  smumullem  15337  phiprmpw  15604  hashgcdeq  15617  prmreclem4  15746  cshws0  15931  pmtrsn  18060  efgsfo  18273  00lsp  19104  dsmm0cl  20207  ordthauslem  21310  pthaus  21564  xkohaus  21579  hmeofval  21684  mumul  25027  musum  25037  ppiub  25049  lgsquadlem2  25226  umgrnloop0  26124  lfgrnloop  26140  numedglnl  26159  usgrnloop0ALT  26217  lfuhgr1v0e  26266  nbuhgr  26359  nbumgr  26363  uhgrnbgr0nb  26370  nbgr0vtxlem  26371  vtxd0nedgb  26515  vtxdusgr0edgnelALT  26523  1loopgrnb0  26529  usgrvd0nedg  26560  vtxdginducedm1lem4  26569  wwlks  26859  iswwlksnon  26878  iswspthsnon  26882  0enwwlksnge1  26894  wspn0  26965  rusgr0edg  27016  clwwlk  27027  clwwlkn  27072  clwwlkn0  27076  clwwlknon  27156  clwwlknon1nloop  27168  clwwlknondisj  27181  clwwlknondisjOLD  27185  vdn0conngrumgrv2  27269  eupth2lemb  27310  eulercrct  27315  frgrregorufr0  27399  numclwwlk3lemOLD  27471  numclwwlk3lem  27473  ofldchr  30044  measvuni  30507  dya2iocuni  30575  repr0  30919  reprlt  30927  reprgt  30929  subfacp1lem6  31395  frpomin  31965  frpomin2  31966  poimirlem26  33667  poimirlem27  33668  cnambfre  33690  itg2addnclem2  33694  areacirclem5  33736  0dioph  37761  undisjrab  38924  supminfxr  40109  dvnprodlem3  40583  pimltmnf2  41334  pimconstlt0  41337  pimgtpnf2  41340  rmsupp0  42576  lcoc0  42638