Theorem rexeqbid

Description: Equality deduction for restricted existential quantifier. See rexeqbidv 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	rexeqbid	|- ( ph -> ( E. x e. A ps <-> E. 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	rexeqf	|- ( A = B -> ( E. x e. A ps <-> E. x e. B ps ) )
7	4 6	syl	|- ( ph -> ( E. x e. A ps <-> E. x e. B ps ) )
8	1 5	rexbid	|- ( ph -> ( E. x e. B ps <-> E. x e. B ch ) )
9	7 8	bitrd	|- ( ph -> ( E. x e. A ps <-> E. x e. B ch ) )