Theorem rexeqbii

Description: Equality deduction for restricted existential quantifier, changing both formula and quantifier domain. Inference form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	rexeqbii.1	|- A = B
	rexeqbii.2	|- ( ps <-> ch )
Assertion	rexeqbii	|- ( E. x e. A ps <-> E. x e. B ch )

Proof

Step	Hyp	Ref	Expression
1		rexeqbii.1	|- A = B
2		rexeqbii.2	|- ( ps <-> ch )
3	1	eleq2i	|- ( x e. A <-> x e. B )
4	3 2	anbi12i	|- ( ( x e. A /\ ps ) <-> ( x e. B /\ ch ) )
5	4	rexbii2	|- ( E. x e. A ps <-> E. x e. B ch )