Theorem raleq 2743

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1398  ∀wral 2522

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527

This theorem is referenced by:  raleqi  2747  raleqdv  2749  raleqbi1dv  2755  sbralie  2798  inteq  3957  iineq1  4010  bnd2  4291  frforeq2  4471  weeq2  4483  ordeq  4498  reg2exmid  4663  reg3exmid  4707  omsinds  4749  fncnv  5427  funimaexglem  5444  isoeq4  5983  acexmidlemv  6056  tfrlem1  6552  tfr0dm  6566  tfrlemisucaccv  6569  tfrlemi1  6576  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemsucaccv  6585  tfr1onlemaccex  6592  tfr1onlemres  6593  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemaccex  6605  tfrcllemres  6606  tfrcldm  6607  ixpeq1  6957  ac6sfi  7168  fimax2gtri  7172  dcfi  7281  supeq1  7290  supeq2  7293  nnnninfeq2  7433  isomni  7440  ismkv  7457  iswomni  7469  acneq  7522  papeq2  7574  tapeq2  7583  sup3exmid  9248  rexanuz  11698  rexfiuz  11699  fimaxre2  11937  modfsummod  12169  mhmpropd  13721  isghm  13996  iscmn  14046  srgideu  14215  dfrhm2  14399  cnprcl2k  15197  ispsmet  15314  ismet  15335  isxmet  15336  cncfval  15563  dvcn  15691  setindis  16863  bdsetindis  16865  strcoll2  16879  strcollnfALT  16882