Theorem raleqbi1dv 2660

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

Hypothesis

Ref	Expression
raleqd.1	|- ( A = B -> ( ph <-> ps ) )

Assertion

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

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem raleqbi1dv

Step	Hyp	Ref	Expression
1		raleq 2652	. 2 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )
2		raleqd.1	. . 3 |- ( A = B -> ( ph <-> ps ) )
3	2	ralbidv 2457	. 2 |- ( A = B -> ( A. x e. B ph <-> A. x e. B ps ) )
4	1, 3	bitrd 187	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ps ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1335   A.wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440

This theorem is referenced by:  frforeq2  4305  weeq2  4317  peano5  4556  isoeq4  5751  exmidomni  7079  pitonn  7762  peano1nnnn  7766  peano2nnnn  7767  peano5nnnn  7806  peano5nni  8830  1nn  8838  peano2nn  8839  dfuzi  9268  istopg  12368  isbasisg  12413  basis2  12417  eltg2  12424  ispsmet  12694  ismet  12715  isxmet  12716  metrest  12877  cncfval  12930  bj-indeq  13475  bj-nntrans  13497