Theorem raleq 2749

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  raleqi  2753  raleqdv  2755  raleqbi1dv  2761  sbralie  2804  inteq  3973  iineq1  4026  bnd2  4310  frforeq2  4490  weeq2  4502  ordeq  4517  reg2exmid  4683  reg3exmid  4727  omsinds  4769  fncnv  5447  funimaexglem  5464  isoeq4  6010  acexmidlemv  6083  tfrlem1  6579  tfr0dm  6593  tfrlemisucaccv  6596  tfrlemi1  6603  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemsucaccv  6612  tfr1onlemaccex  6619  tfr1onlemres  6620  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemaccex  6632  tfrcllemres  6633  tfrcldm  6634  ixpeq1  6991  ac6sfi  7202  fimax2gtri  7206  dcfi  7315  supeq1  7326  supeq2  7329  nnnninfeq2  7469  isomni  7476  ismkv  7493  iswomni  7505  acneq  7558  papeq2  7610  tapeq2  7619  sup3exmid  9287  rexanuz  11754  rexfiuz  11755  fimaxre2  11993  modfsummod  12225  mhmpropd  13773  isghm  14046  iscmn  14096  srgideu  14276  dfrhm2  14461  cnprcl2k  15307  ispsmet  15424  ismet  15445  isxmet  15446  cncfval  15673  dvcn  15801  setindis  16993  bdsetindis  16995  strcoll2  17009  strcollnfALT  17012