Theorem raleq 2673

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ∀wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  raleqi  2677  raleqdv  2679  raleqbi1dv  2681  sbralie  2723  inteq  3849  iineq1  3902  bnd2  4175  frforeq2  4347  weeq2  4359  ordeq  4374  reg2exmid  4537  reg3exmid  4581  omsinds  4623  fncnv  5284  funimaexglem  5301  isoeq4  5807  acexmidlemv  5875  tfrlem1  6311  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemi1  6335  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemsucaccv  6344  tfr1onlemaccex  6351  tfr1onlemres  6352  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemaccex  6364  tfrcllemres  6365  tfrcldm  6366  ixpeq1  6711  ac6sfi  6900  fimax2gtri  6903  dcfi  6982  supeq1  6987  supeq2  6990  nnnninfeq2  7129  isomni  7136  ismkv  7153  iswomni  7165  tapeq2  7254  sup3exmid  8916  rexanuz  10999  rexfiuz  11000  fimaxre2  11237  modfsummod  11468  mhmpropd  12862  iscmn  13101  srgideu  13160  cnprcl2k  13791  ispsmet  13908  ismet  13929  isxmet  13930  cncfval  14144  dvcn  14249  setindis  14804  bdsetindis  14806  strcoll2  14820  strcollnfALT  14823