Theorem rabeq0 4349

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

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541   ∈ wcel 2106  {cab 2708  ∀wral 3060  {crab 3405  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-ral 3061  df-rab 3406  df-dif 3916  df-nul 4288

This theorem is referenced by:  rabn0  4350  rabnc  4352  dffr2ALT  5603  wereu2  5635  frpomin  6299  frpomin2  6300  tz6.26OLD  6307  fndmdifeq0  6999  fnnfpeq0  7129  wemapso2  9498  wemapwe  9642  hashbclem  14361  hashbc  14362  wrdnfi  14448  smuval2  16373  smupvallem  16374  smu01lem  16376  smumullem  16383  phiprmpw  16659  hashgcdeq  16672  prmreclem4  16802  cshws0  16985  pmtrsn  19315  efgsfo  19535  00lsp  20499  dsmm0cl  21183  ordthauslem  22771  pthaus  23026  xkohaus  23041  hmeofval  23146  mumul  26567  musum  26577  ppiub  26589  lgsquadlem2  26766  umgrnloop0  28123  lfgrnloop  28139  numedglnl  28158  usgrnloop0ALT  28216  lfuhgr1v0e  28265  nbuhgr  28354  nbumgr  28358  uhgrnbgr0nb  28365  nbgr0vtxlem  28366  vtxd0nedgb  28499  vtxdusgr0edgnelALT  28507  1loopgrnb0  28513  usgrvd0nedg  28544  vtxdginducedm1lem4  28553  wwlks  28843  iswwlksnon  28861  iswspthsnon  28864  0enwwlksnge1  28872  wspn0  28932  rusgr0edg  28981  clwwlk  28990  clwwlkn  29033  clwwlkn0  29035  clwwlknon  29097  clwwlknon1nloop  29106  clwwlknondisj  29118  vdn0conngrumgrv2  29203  eupth2lemb  29244  eulercrct  29249  frgrregorufr0  29331  numclwwlk3lem2  29391  ofldchr  32180  zarcls1  32539  measvuni  32902  dya2iocuni  32972  repr0  33313  reprlt  33321  reprgt  33323  nummin  33784  subfacp1lem6  33866  prv1n  34112  poimirlem26  36177  poimirlem27  36178  cnambfre  36199  itg2addnclem2  36203  areacirclem5  36243  sticksstones1  40627  nna4b4nsq  41056  0dioph  41159  undisjrab  42708  supminfxr  43819  dvnprodlem3  44309  pimltmnf2f  45058  pimconstlt0  45062  pimgtpnf2f  45066  rmsupp0  46564  lcoc0  46623  rrxsphere  46954