Theorem raleq 2730

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  raleqi  2734  raleqdv  2736  raleqbi1dv  2742  sbralie  2785  inteq  3931  iineq1  3984  bnd2  4263  frforeq2  4442  weeq2  4454  ordeq  4469  reg2exmid  4634  reg3exmid  4678  omsinds  4720  fncnv  5396  funimaexglem  5413  isoeq4  5944  acexmidlemv  6015  tfrlem1  6473  tfr0dm  6487  tfrlemisucaccv  6490  tfrlemi1  6497  tfrlemi14d  6498  tfrexlem  6499  tfr1onlemsucaccv  6506  tfr1onlemaccex  6513  tfr1onlemres  6514  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemaccex  6526  tfrcllemres  6527  tfrcldm  6528  ixpeq1  6877  ac6sfi  7086  fimax2gtri  7090  dcfi  7179  supeq1  7184  supeq2  7187  nnnninfeq2  7327  isomni  7334  ismkv  7351  iswomni  7363  acneq  7416  tapeq2  7471  sup3exmid  9136  rexanuz  11548  rexfiuz  11549  fimaxre2  11787  modfsummod  12018  mhmpropd  13548  isghm  13829  iscmn  13879  srgideu  13984  dfrhm2  14167  cnprcl2k  14929  ispsmet  15046  ismet  15067  isxmet  15068  cncfval  15295  dvcn  15423  setindis  16562  bdsetindis  16564  strcoll2  16578  strcollnfALT  16581