Theorem rabeq0 4315

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 4305	. 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
2		df-rab 3072	. . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
3	2	eqeq1i 2743	. 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅)
4		raln 3080	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑))
5	1, 3, 4	3bitr4i 302	1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  {crab 3067  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-rab 3072  df-dif 3886  df-nul 4254

This theorem is referenced by:  rabn0  4316  rabnc  4318  dffr2ALT  5545  wereu2  5577  frpomin  6228  frpomin2  6229  tz6.26OLD  6236  fndmdifeq0  6903  fnnfpeq0  7032  wemapso2  9242  wemapwe  9385  hashbclem  14092  hashbc  14093  wrdnfi  14179  smuval2  16117  smupvallem  16118  smu01lem  16120  smumullem  16127  phiprmpw  16405  hashgcdeq  16418  prmreclem4  16548  cshws0  16731  pmtrsn  19042  efgsfo  19260  00lsp  20158  dsmm0cl  20857  ordthauslem  22442  pthaus  22697  xkohaus  22712  hmeofval  22817  mumul  26235  musum  26245  ppiub  26257  lgsquadlem2  26434  umgrnloop0  27382  lfgrnloop  27398  numedglnl  27417  usgrnloop0ALT  27475  lfuhgr1v0e  27524  nbuhgr  27613  nbumgr  27617  uhgrnbgr0nb  27624  nbgr0vtxlem  27625  vtxd0nedgb  27758  vtxdusgr0edgnelALT  27766  1loopgrnb0  27772  usgrvd0nedg  27803  vtxdginducedm1lem4  27812  wwlks  28101  iswwlksnon  28119  iswspthsnon  28122  0enwwlksnge1  28130  wspn0  28190  rusgr0edg  28239  clwwlk  28248  clwwlkn  28291  clwwlkn0  28293  clwwlknon  28355  clwwlknon1nloop  28364  clwwlknondisj  28376  vdn0conngrumgrv2  28461  eupth2lemb  28502  eulercrct  28507  frgrregorufr0  28589  numclwwlk3lem2  28649  ofldchr  31415  zarcls1  31721  measvuni  32082  dya2iocuni  32150  repr0  32491  reprlt  32499  reprgt  32501  nummin  32963  subfacp1lem6  33047  prv1n  33293  poimirlem26  35730  poimirlem27  35731  cnambfre  35752  itg2addnclem2  35756  areacirclem5  35796  sticksstones1  40030  nna4b4nsq  40413  0dioph  40516  undisjrab  41813  supminfxr  42894  dvnprodlem3  43379  pimltmnf2  44125  pimconstlt0  44128  pimgtpnf2  44131  rmsupp0  45592  lcoc0  45651  rrxsphere  45982