Theorem rabeq0 4385

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542   ∈ wcel 2107  {cab 2710  ∀wral 3062  {crab 3433  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-rab 3434  df-dif 3952  df-nul 4324

This theorem is referenced by:  rabn0  4386  rabnc  4388  dffr2ALT  5642  wereu2  5674  frpomin  6342  frpomin2  6343  tz6.26OLD  6350  fndmdifeq0  7046  fnnfpeq0  7176  wemapso2  9548  wemapwe  9692  hashbclem  14411  hashbc  14412  wrdnfi  14498  smuval2  16423  smupvallem  16424  smu01lem  16426  smumullem  16433  phiprmpw  16709  hashgcdeq  16722  prmreclem4  16852  cshws0  17035  pmtrsn  19387  efgsfo  19607  00lsp  20592  dsmm0cl  21295  ordthauslem  22887  pthaus  23142  xkohaus  23157  hmeofval  23262  mumul  26685  musum  26695  ppiub  26707  lgsquadlem2  26884  umgrnloop0  28369  lfgrnloop  28385  numedglnl  28404  usgrnloop0ALT  28462  lfuhgr1v0e  28511  nbuhgr  28600  nbumgr  28604  uhgrnbgr0nb  28611  nbgr0vtxlem  28612  vtxd0nedgb  28745  vtxdusgr0edgnelALT  28753  1loopgrnb0  28759  usgrvd0nedg  28790  vtxdginducedm1lem4  28799  wwlks  29089  iswwlksnon  29107  iswspthsnon  29110  0enwwlksnge1  29118  wspn0  29178  rusgr0edg  29227  clwwlk  29236  clwwlkn  29279  clwwlkn0  29281  clwwlknon  29343  clwwlknon1nloop  29352  clwwlknondisj  29364  vdn0conngrumgrv2  29449  eupth2lemb  29490  eulercrct  29495  frgrregorufr0  29577  numclwwlk3lem2  29637  ofldchr  32432  zarcls1  32849  measvuni  33212  dya2iocuni  33282  repr0  33623  reprlt  33631  reprgt  33633  nummin  34094  subfacp1lem6  34176  prv1n  34422  poimirlem26  36514  poimirlem27  36515  cnambfre  36536  itg2addnclem2  36540  areacirclem5  36580  sticksstones1  40962  nna4b4nsq  41402  0dioph  41516  undisjrab  43065  supminfxr  44174  dvnprodlem3  44664  pimltmnf2f  45413  pimconstlt0  45417  pimgtpnf2f  45421  rmsupp0  47044  lcoc0  47103  rrxsphere  47434