Theorem raleq 2701

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1372  ∀wral 2483

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488

This theorem is referenced by:  raleqi  2705  raleqdv  2707  raleqbi1dv  2713  sbralie  2755  inteq  3887  iineq1  3940  bnd2  4216  frforeq2  4391  weeq2  4403  ordeq  4418  reg2exmid  4583  reg3exmid  4627  omsinds  4669  fncnv  5339  funimaexglem  5356  isoeq4  5872  acexmidlemv  5941  tfrlem1  6393  tfr0dm  6407  tfrlemisucaccv  6410  tfrlemi1  6417  tfrlemi14d  6418  tfrexlem  6419  tfr1onlemsucaccv  6426  tfr1onlemaccex  6433  tfr1onlemres  6434  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllemaccex  6446  tfrcllemres  6447  tfrcldm  6448  ixpeq1  6795  ac6sfi  6994  fimax2gtri  6997  dcfi  7082  supeq1  7087  supeq2  7090  nnnninfeq2  7230  isomni  7237  ismkv  7254  iswomni  7266  acneq  7313  tapeq2  7364  sup3exmid  9029  rexanuz  11241  rexfiuz  11242  fimaxre2  11480  modfsummod  11711  mhmpropd  13240  isghm  13521  iscmn  13571  srgideu  13676  dfrhm2  13858  cnprcl2k  14620  ispsmet  14737  ismet  14758  isxmet  14759  cncfval  14986  dvcn  15114  setindis  15836  bdsetindis  15838  strcoll2  15852  strcollnfALT  15855