Theorem raleq 2728

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  ∀wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  raleqi  2732  raleqdv  2734  raleqbi1dv  2740  sbralie  2783  inteq  3925  iineq1  3978  bnd2  4256  frforeq2  4435  weeq2  4447  ordeq  4462  reg2exmid  4627  reg3exmid  4671  omsinds  4713  fncnv  5386  funimaexglem  5403  isoeq4  5927  acexmidlemv  5998  tfrlem1  6452  tfr0dm  6466  tfrlemisucaccv  6469  tfrlemi1  6476  tfrlemi14d  6477  tfrexlem  6478  tfr1onlemsucaccv  6485  tfr1onlemaccex  6492  tfr1onlemres  6493  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllemaccex  6505  tfrcllemres  6506  tfrcldm  6507  ixpeq1  6854  ac6sfi  7056  fimax2gtri  7059  dcfi  7144  supeq1  7149  supeq2  7152  nnnninfeq2  7292  isomni  7299  ismkv  7316  iswomni  7328  acneq  7380  tapeq2  7435  sup3exmid  9100  rexanuz  11494  rexfiuz  11495  fimaxre2  11733  modfsummod  11964  mhmpropd  13494  isghm  13775  iscmn  13825  srgideu  13930  dfrhm2  14112  cnprcl2k  14874  ispsmet  14991  ismet  15012  isxmet  15013  cncfval  15240  dvcn  15368  setindis  16288  bdsetindis  16290  strcoll2  16304  strcollnfALT  16307