Theorem raleq12d 1797

Description: Equality deduction for restricted universal quantifier.

Hypotheses

Ref	Expression
raleq12d.1	|- (ph -> A = B)
raleq12d.2	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
raleq12d	|- (ph -> (A.x e. A ps <-> A.x e. B ch))

Distinct variable groups:   x,A   x,B   ph,x

Proof of Theorem raleq12d

Step	Hyp	Ref	Expression
1		raleq12d.1	. . 3 |- (ph -> A = B)
2	1	raleq1d 1792	. 2 |- (ph -> (A.x e. A ps <-> A.x e. B ps))
3		raleq12d.2	. . 3 |- (ph -> (ps <-> ch))
4	3	ralbidv 1666	. 2 |- (ph -> (A.x e. B ps <-> A.x e. B ch))
5	2, 4	bitrd 530	1 |- (ph -> (A.x e. A ps <-> A.x e. B ch))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958  A.wral 1648

This theorem is referenced by:  climconst3 7096  ishaus 7780  iscms 7943  grpidval 8054  isring 8137  vci 8163  isvclem 8192  isnvlem 8225  nvi 8229  lnoval 8409  ajfval 8465  isphg 8472  spwval2 8649  elghomlem1 10377  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-cleq 1472  df-clel 1475  df-ral 1652

Copyright terms: Public domain