Theorem cbvrexv2

Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution which also changes the quantifier domain. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by David Moews, 1-May-2017) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralv2.1	|- ( x = y -> ( ps <-> ch ) )
2		cbvralv2.2	|- ( x = y -> A = B )
3		nfcv	|- F/_ y A
4		nfcv	|- F/_ x B
5		nfv	|- F/ y ps
6		nfv	|- F/ x ch
7	3 4 5 6 2 1	cbvrexcsf	|- ( E. x e. A ps <-> E. y e. B ch )