Theorem rabeq0 4340

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541   ∈ wcel 2113  {cab 2714  ∀wral 3051  {crab 3399  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-ral 3052  df-rab 3400  df-dif 3904  df-nul 4286

This theorem is referenced by:  rabn0  4341  rabnc  4343  dffr2ALT  5586  wereu2  5621  frpomin  6298  frpomin2  6299  fndmdifeq0  6989  fnnfpeq0  7124  wemapso2  9458  wemapwe  9606  hashbclem  14375  hashbc  14376  wrdnfi  14471  smuval2  16409  smupvallem  16410  smu01lem  16412  smumullem  16419  phiprmpw  16703  hashgcdeq  16717  prmreclem4  16847  cshws0  17029  pmtrsn  19448  efgsfo  19668  00lsp  20932  ofldchr  21531  dsmm0cl  21695  ordthauslem  23327  pthaus  23582  xkohaus  23597  hmeofval  23702  mumul  27147  musum  27157  ppiub  27171  lgsquadlem2  27348  umgrnloop0  29182  lfgrnloop  29198  numedglnl  29217  usgrnloop0ALT  29278  lfuhgr1v0e  29327  nbuhgr  29416  nbumgr  29420  uhgrnbgr0nb  29427  nbgr0edglem  29429  vtxd0nedgb  29562  vtxdusgr0edgnelALT  29570  1loopgrnb0  29576  usgrvd0nedg  29607  vtxdginducedm1lem4  29616  wwlks  29908  iswwlksnon  29926  iswspthsnon  29929  0enwwlksnge1  29937  wspn0  29997  rusgr0edg  30049  clwwlk  30058  clwwlkn  30101  clwwlkn0  30103  clwwlknon  30165  clwwlknon1nloop  30174  clwwlknondisj  30186  vdn0conngrumgrv2  30271  eupth2lemb  30312  eulercrct  30317  frgrregorufr0  30399  numclwwlk3lem2  30459  esplyfval2  33723  2sqr3minply  33937  cos9thpiminply  33945  zarcls1  34026  measvuni  34371  dya2iocuni  34440  repr0  34768  reprlt  34776  reprgt  34778  nummin  35249  fineqvnttrclselem1  35277  subfacp1lem6  35379  prv1n  35625  poimirlem26  37847  poimirlem27  37848  cnambfre  37869  itg2addnclem2  37873  areacirclem5  37913  sticksstones1  42400  nna4b4nsq  42903  0dioph  43020  undisjrab  44547  supminfxr  45708  dvnprodlem3  46192  pimltmnf2f  46941  pimconstlt0  46945  pimgtpnf2f  46949  isubgr0uhgr  48119  stgr0  48206  rmsupp0  48614  lcoc0  48668  rrxsphere  48994