Theorem raleq 2598

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 2253	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2253	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 2594	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1312  ∀wral 2388

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393

This theorem is referenced by:  raleqi  2602  raleqdv  2604  raleqbi1dv  2606  sbralie  2639  inteq  3738  iineq1  3791  bnd2  4055  frforeq2  4225  weeq2  4237  ordeq  4252  reg2exmid  4409  reg3exmid  4452  omsinds  4493  fncnv  5145  funimaexglem  5162  isoeq4  5657  acexmidlemv  5724  tfrlem1  6157  tfr0dm  6171  tfrlemisucaccv  6174  tfrlemi1  6181  tfrlemi14d  6182  tfrexlem  6183  tfr1onlemsucaccv  6190  tfr1onlemaccex  6197  tfr1onlemres  6198  tfrcllemsucaccv  6203  tfrcllembxssdm  6205  tfrcllemaccex  6210  tfrcllemres  6211  tfrcldm  6212  ixpeq1  6555  ac6sfi  6743  fimax2gtri  6746  supeq1  6823  supeq2  6826  isomni  6956  ismkv  6975  sup3exmid  8619  rexanuz  10646  rexfiuz  10647  fimaxre2  10884  modfsummod  11113  cnprcl2k  12211  ispsmet  12306  ismet  12327  isxmet  12328  cncfval  12539  dvcn  12613  setindis  12848  bdsetindis  12850  strcoll2  12864