Theorem raleqbid

Description: Equality deduction for restricted universal quantifier. See raleqbidv for a version based on fewer axioms. (Contributed by Thierry Arnoux, 8-Mar-2017)

	Ref	Expression
Hypotheses	raleqbid.0	|- F/ x ph
	raleqbid.1	|- F/_ x A
	raleqbid.2	|- F/_ x B
	raleqbid.3	|- ( ph -> A = B )
	raleqbid.4	|- ( ph -> ( ps <-> ch ) )
Assertion	raleqbid	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Proof

Step	Hyp	Ref	Expression
1		raleqbid.0	|- F/ x ph
2		raleqbid.1	|- F/_ x A
3		raleqbid.2	|- F/_ x B
4		raleqbid.3	|- ( ph -> A = B )
5		raleqbid.4	|- ( ph -> ( ps <-> ch ) )
6	2 3	raleqf	|- ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
7	4 6	syl	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )
8	1 5	ralbid	|- ( ph -> ( A. x e. B ps <-> A. x e. B ch ) )
9	7 8	bitrd	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )