Theorem raleq 2705

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Assertion

Ref	Expression
raleq	|- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2350	. 2 |- F/_ x A
2		nfcv 2350	. 2 |- F/_ x B
3	1, 2	raleqf 2701	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   A.wral 2486

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491

This theorem is referenced by:  raleqi  2709  raleqdv  2711  raleqbi1dv  2717  sbralie  2760  inteq  3902  iineq1  3955  bnd2  4233  frforeq2  4410  weeq2  4422  ordeq  4437  reg2exmid  4602  reg3exmid  4646  omsinds  4688  fncnv  5359  funimaexglem  5376  isoeq4  5896  acexmidlemv  5965  tfrlem1  6417  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemi1  6441  tfrlemi14d  6442  tfrexlem  6443  tfr1onlemsucaccv  6450  tfr1onlemaccex  6457  tfr1onlemres  6458  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemaccex  6470  tfrcllemres  6471  tfrcldm  6472  ixpeq1  6819  ac6sfi  7021  fimax2gtri  7024  dcfi  7109  supeq1  7114  supeq2  7117  nnnninfeq2  7257  isomni  7264  ismkv  7281  iswomni  7293  acneq  7345  tapeq2  7400  sup3exmid  9065  rexanuz  11414  rexfiuz  11415  fimaxre2  11653  modfsummod  11884  mhmpropd  13413  isghm  13694  iscmn  13744  srgideu  13849  dfrhm2  14031  cnprcl2k  14793  ispsmet  14910  ismet  14931  isxmet  14932  cncfval  15159  dvcn  15287  setindis  16102  bdsetindis  16104  strcoll2  16118  strcollnfALT  16121