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  5945  acexmidlemv  6016  tfrlem1  6474  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemi1  6498  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemsucaccv  6507  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  ixpeq1  6878  ac6sfi  7087  fimax2gtri  7091  dcfi  7180  supeq1  7185  supeq2  7188  nnnninfeq2  7328  isomni  7335  ismkv  7352  iswomni  7364  acneq  7417  tapeq2  7472  sup3exmid  9137  rexanuz  11553  rexfiuz  11554  fimaxre2  11792  modfsummod  12024  mhmpropd  13554  isghm  13835  iscmn  13885  srgideu  13991  dfrhm2  14174  cnprcl2k  14936  ispsmet  15053  ismet  15074  isxmet  15075  cncfval  15302  dvcn  15430  setindis  16588  bdsetindis  16590  strcoll2  16604  strcollnfALT  16607