Theorem raleqbi1dv 2714

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 2702	. 2 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )
2		raleqd.1	. . 3 |- ( A = B -> ( ph <-> ps ) )
3	2	ralbidv 2506	. 2 |- ( A = B -> ( A. x e. B ph <-> A. x e. B ps ) )
4	1, 3	bitrd 188	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ps ) )

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  frforeq2  4393  weeq2  4405  peano5  4647  isoeq4  5875  exmidomni  7246  tapeq2  7367  pitonn  7963  peano1nnnn  7967  peano2nnnn  7968  peano5nnnn  8007  peano5nni  9041  1nn  9049  peano2nn  9050  dfuzi  9485  mhmpropd  13331  issubm  13337  isghm  13612  ghmeql  13636  iscmn  13662  dfrhm2  13949  islssm  14152  islssmg  14153  istopg  14504  isbasisg  14549  basis2  14553  eltg2  14558  ispsmet  14828  ismet  14849  isxmet  14850  metrest  15011  cncfval  15077  bj-indeq  15902  bj-nntrans  15924