Theorem rexxpf

Description: Version of rexxp with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	ralxpf.1	|- F/ y ph
	ralxpf.2	|- F/ z ph
	ralxpf.3	|- F/ x ps
	ralxpf.4	|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion	rexxpf	|- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )

Proof

Step	Hyp	Ref	Expression
1		ralxpf.1	|- F/ y ph
2		ralxpf.2	|- F/ z ph
3		ralxpf.3	|- F/ x ps
4		ralxpf.4	|- ( x = <. y , z >. -> ( ph <-> ps ) )
5	1	nfn	|- F/ y -. ph
6	2	nfn	|- F/ z -. ph
7	3	nfn	|- F/ x -. ps
8	4	notbid	|- ( x = <. y , z >. -> ( -. ph <-> -. ps ) )
9	5 6 7 8	ralxpf	|- ( A. x e. ( A X. B ) -. ph <-> A. y e. A A. z e. B -. ps )
10		ralnex	|- ( A. z e. B -. ps <-> -. E. z e. B ps )
11	10	ralbii	|- ( A. y e. A A. z e. B -. ps <-> A. y e. A -. E. z e. B ps )
12	9 11	bitri	|- ( A. x e. ( A X. B ) -. ph <-> A. y e. A -. E. z e. B ps )
13	12	notbii	|- ( -. A. x e. ( A X. B ) -. ph <-> -. A. y e. A -. E. z e. B ps )
14		dfrex2	|- ( E. x e. ( A X. B ) ph <-> -. A. x e. ( A X. B ) -. ph )
15		dfrex2	|- ( E. y e. A E. z e. B ps <-> -. A. y e. A -. E. z e. B ps )
16	13 14 15	3bitr4i	|- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )