Theorem raleq 2554

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Assertion

Ref	Expression
raleq	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2223	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2223	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 2550	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1285  ∀wral 2353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358

This theorem is referenced by:  raleqi  2558  raleqdv  2560  raleqbi1dv  2562  sbralie  2595  inteq  3659  iineq1  3712  bnd2  3967  frforeq2  4128  weeq2  4140  ordeq  4155  reg2exmid  4307  reg3exmid  4350  fncnv  5016  funimaexglem  5033  isoeq4  5496  acexmidlemv  5562  tfrlem1  5978  tfr0dm  5992  tfrlemisucaccv  5995  tfrlemi1  6002  tfrlemi14d  6003  tfrexlem  6004  tfr1onlemsucaccv  6011  tfr1onlemaccex  6018  tfr1onlemres  6019  tfrcllemsucaccv  6024  tfrcllembxssdm  6026  tfrcllemaccex  6031  tfrcllemres  6032  tfrcldm  6033  ac6sfi  6455  supeq1  6494  supeq2  6497  rexanuz  10093  rexfiuz  10094  fimaxre2  10328  setindis  11047  bdsetindis  11049  strcoll2  11063