Theorem rabeq0 4329

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

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  {crab 3390  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-rab 3391  df-dif 3893  df-nul 4275

This theorem is referenced by:  rabn0  4330  rabnc  4332  dffr2ALT  5587  wereu2  5622  frpomin  6299  frpomin2  6300  fndmdifeq0  6991  fnnfpeq0  7127  wemapso2  9462  wemapwe  9612  hashbclem  14408  hashbc  14409  wrdnfi  14504  smuval2  16445  smupvallem  16446  smu01lem  16448  smumullem  16455  phiprmpw  16740  hashgcdeq  16754  prmreclem4  16884  cshws0  17066  pmtrsn  19488  efgsfo  19708  00lsp  20970  ofldchr  21569  dsmm0cl  21733  ordthauslem  23361  pthaus  23616  xkohaus  23631  hmeofval  23736  mumul  27161  musum  27171  ppiub  27184  lgsquadlem2  27361  umgrnloop0  29195  lfgrnloop  29211  numedglnl  29230  usgrnloop0ALT  29291  lfuhgr1v0e  29340  nbuhgr  29429  nbumgr  29433  uhgrnbgr0nb  29440  nbgr0edglem  29442  vtxd0nedgb  29575  vtxdusgr0edgnelALT  29583  1loopgrnb0  29589  usgrvd0nedg  29620  vtxdginducedm1lem4  29629  wwlks  29921  iswwlksnon  29939  iswspthsnon  29942  0enwwlksnge1  29950  wspn0  30010  rusgr0edg  30062  clwwlk  30071  clwwlkn  30114  clwwlkn0  30116  clwwlknon  30178  clwwlknon1nloop  30187  clwwlknondisj  30199  vdn0conngrumgrv2  30284  eupth2lemb  30325  eulercrct  30330  frgrregorufr0  30412  numclwwlk3lem2  30472  esplyfval2  33727  2sqr3minply  33943  cos9thpiminply  33951  zarcls1  34032  measvuni  34377  dya2iocuni  34446  repr0  34774  reprlt  34782  reprgt  34784  nummin  35255  fineqvnttrclselem1  35284  subfacp1lem6  35386  prv1n  35632  poimirlem26  37984  poimirlem27  37985  cnambfre  38006  itg2addnclem2  38010  areacirclem5  38050  sticksstones1  42602  nna4b4nsq  43110  0dioph  43227  undisjrab  44754  supminfxr  45913  dvnprodlem3  46397  pimltmnf2f  47146  pimconstlt0  47150  pimgtpnf2f  47154  isubgr0uhgr  48364  stgr0  48451  rmsupp0  48859  lcoc0  48913  rrxsphere  49239