Theorem rabeq0 4187

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 4182	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3099	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2783	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3173	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 295	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601   ∈ wcel 2107  {cab 2763  ∀wral 3090  {crab 3094  ∅c0 4141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rab 3099  df-dif 3795  df-nul 4142

This theorem is referenced by:  rabn0  4188  rabnc  4190  dffr2  5322  frc  5323  frirr  5334  wereu2  5354  tz6.26  5966  fndmdifeq0  6588  fnnfpeq0  6713  wemapso2  8749  wemapwe  8893  hashbclem  13556  hashbc  13557  wrdnfi  13643  smuval2  15620  smupvallem  15621  smu01lem  15623  smumullem  15630  phiprmpw  15896  hashgcdeq  15909  prmreclem4  16038  cshws0  16218  pmtrsn  18334  efgsfo  18548  00lsp  19387  dsmm0cl  20494  ordthauslem  21606  pthaus  21861  xkohaus  21876  hmeofval  21981  mumul  25370  musum  25380  ppiub  25392  lgsquadlem2  25569  umgrnloop0  26474  lfgrnloop  26490  numedglnl  26510  usgrnloop0ALT  26568  lfuhgr1v0e  26618  nbuhgr  26707  nbumgr  26711  uhgrnbgr0nb  26718  nbgr0vtxlem  26719  vtxd0nedgb  26853  vtxdusgr0edgnelALT  26861  1loopgrnb0  26867  usgrvd0nedg  26898  vtxdginducedm1lem4  26907  wwlks  27201  iswwlksnon  27219  iswspthsnon  27222  0enwwlksnge1  27230  wspn0  27321  rusgr0edg  27370  clwwlk  27380  clwwlkn  27432  clwwlkn0  27434  clwwlknon  27509  clwwlknon1nloop  27518  clwwlknondisj  27530  vdn0conngrumgrv2  27616  eupth2lemb  27658  eulercrct  27663  frgrregorufr0  27749  numclwwlk3lem2  27833  ofldchr  30384  measvuni  30883  dya2iocuni  30951  repr0  31299  reprlt  31307  reprgt  31309  subfacp1lem6  31774  frpomin  32335  frpomin2  32336  poimirlem26  34070  poimirlem27  34071  cnambfre  34092  itg2addnclem2  34096  areacirclem5  34138  0dioph  38316  undisjrab  39475  supminfxr  40613  dvnprodlem3  41105  pimltmnf2  41852  pimconstlt0  41855  pimgtpnf2  41858  rmsupp0  43178  lcoc0  43240  rrxsphere  43498