Theorem rabeq0 4336

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 4331	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3145	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2824	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3153	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 305	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 398  ∀wal 1529   = wceq 1531   ∈ wcel 2108  {cab 2797  ∀wral 3136  {crab 3140  ∅c0 4289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rab 3145  df-dif 3937  df-nul 4290

This theorem is referenced by:  rabn0  4337  rabnc  4339  dffr2  5513  frc  5514  frirr  5525  wereu2  5545  tz6.26  6172  fndmdifeq0  6807  fnnfpeq0  6933  wemapso2  9009  wemapwe  9152  hashbclem  13802  hashbc  13803  wrdnfi  13891  smuval2  15823  smupvallem  15824  smu01lem  15826  smumullem  15833  phiprmpw  16105  hashgcdeq  16118  prmreclem4  16247  cshws0  16427  pmtrsn  18639  efgsfo  18857  00lsp  19745  dsmm0cl  20876  ordthauslem  21983  pthaus  22238  xkohaus  22253  hmeofval  22358  mumul  25750  musum  25760  ppiub  25772  lgsquadlem2  25949  umgrnloop0  26886  lfgrnloop  26902  numedglnl  26921  usgrnloop0ALT  26979  lfuhgr1v0e  27028  nbuhgr  27117  nbumgr  27121  uhgrnbgr0nb  27128  nbgr0vtxlem  27129  vtxd0nedgb  27262  vtxdusgr0edgnelALT  27270  1loopgrnb0  27276  usgrvd0nedg  27307  vtxdginducedm1lem4  27316  wwlks  27605  iswwlksnon  27623  iswspthsnon  27626  0enwwlksnge1  27634  wspn0  27695  rusgr0edg  27744  clwwlk  27753  clwwlkn  27796  clwwlkn0  27798  clwwlknon  27861  clwwlknon1nloop  27870  clwwlknondisj  27882  vdn0conngrumgrv2  27967  eupth2lemb  28008  eulercrct  28013  frgrregorufr0  28095  numclwwlk3lem2  28155  ofldchr  30880  measvuni  31466  dya2iocuni  31534  repr0  31875  reprlt  31883  reprgt  31885  subfacp1lem6  32425  prv1n  32671  frpomin  33071  frpomin2  33072  poimirlem26  34910  poimirlem27  34911  cnambfre  34932  itg2addnclem2  34936  areacirclem5  34978  0dioph  39365  undisjrab  40628  supminfxr  41729  dvnprodlem3  42222  pimltmnf2  42969  pimconstlt0  42972  pimgtpnf2  42975  rmsupp0  44406  lcoc0  44467  rrxsphere  44725