Theorem sbcreu

Description: Interchange class substitution and restricted unique existential quantifier. (Contributed by NM, 24-Feb-2013) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcreu	|- ( [. A / x ]. E! y e. B ph <-> E! y e. B [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / x ]. E! y e. B ph -> A e. _V )
2		reurex	|- ( E! y e. B [. A / x ]. ph -> E. y e. B [. A / x ]. ph )
3		sbcex	|- ( [. A / x ]. ph -> A e. _V )
4	3	rexlimivw	|- ( E. y e. B [. A / x ]. ph -> A e. _V )
5	2 4	syl	|- ( E! y e. B [. A / x ]. ph -> A e. _V )
6		dfsbcq2	|- ( z = A -> ( [ z / x ] E! y e. B ph <-> [. A / x ]. E! y e. B ph ) )
7		dfsbcq2	|- ( z = A -> ( [ z / x ] ph <-> [. A / x ]. ph ) )
8	7	reubidv	|- ( z = A -> ( E! y e. B [ z / x ] ph <-> E! y e. B [. A / x ]. ph ) )
9		nfcv	|- F/_ x B
10		nfs1v	|- F/ x [ z / x ] ph
11	9 10	nfreuw	|- F/ x E! y e. B [ z / x ] ph
12		sbequ12	|- ( x = z -> ( ph <-> [ z / x ] ph ) )
13	12	reubidv	|- ( x = z -> ( E! y e. B ph <-> E! y e. B [ z / x ] ph ) )
14	11 13	sbiev	|- ( [ z / x ] E! y e. B ph <-> E! y e. B [ z / x ] ph )
15	6 8 14	vtoclbg	|- ( A e. _V -> ( [. A / x ]. E! y e. B ph <-> E! y e. B [. A / x ]. ph ) )
16	1 5 15	pm5.21nii	|- ( [. A / x ]. E! y e. B ph <-> E! y e. B [. A / x ]. ph )