Theorem bnj89

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj89.1	|- Z e. _V
Assertion	bnj89	|- ( [. Z / y ]. E! x ph <-> E! x [. Z / y ]. ph )

Proof

Step	Hyp	Ref	Expression
1		bnj89.1	|- Z e. _V
2		sbcex2	|- ( [. Z / y ]. E. w A. x ( ph <-> x = w ) <-> E. w [. Z / y ]. A. x ( ph <-> x = w ) )
3		sbcal	|- ( [. Z / y ]. A. x ( ph <-> x = w ) <-> A. x [. Z / y ]. ( ph <-> x = w ) )
4	3	exbii	|- ( E. w [. Z / y ]. A. x ( ph <-> x = w ) <-> E. w A. x [. Z / y ]. ( ph <-> x = w ) )
5		sbcbig	|- ( Z e. _V -> ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) ) )
6	1 5	ax-mp	|- ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) )
7		sbcg	|- ( Z e. _V -> ( [. Z / y ]. x = w <-> x = w ) )
8	1 7	ax-mp	|- ( [. Z / y ]. x = w <-> x = w )
9	8	bibi2i	|- ( ( [. Z / y ]. ph <-> [. Z / y ]. x = w ) <-> ( [. Z / y ]. ph <-> x = w ) )
10	6 9	bitri	|- ( [. Z / y ]. ( ph <-> x = w ) <-> ( [. Z / y ]. ph <-> x = w ) )
11	10	albii	|- ( A. x [. Z / y ]. ( ph <-> x = w ) <-> A. x ( [. Z / y ]. ph <-> x = w ) )
12	11	exbii	|- ( E. w A. x [. Z / y ]. ( ph <-> x = w ) <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
13	2 4 12	3bitri	|- ( [. Z / y ]. E. w A. x ( ph <-> x = w ) <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
14		eu6	|- ( E! x ph <-> E. w A. x ( ph <-> x = w ) )
15	14	sbcbii	|- ( [. Z / y ]. E! x ph <-> [. Z / y ]. E. w A. x ( ph <-> x = w ) )
16		eu6	|- ( E! x [. Z / y ]. ph <-> E. w A. x ( [. Z / y ]. ph <-> x = w ) )
17	13 15 16	3bitr4i	|- ( [. Z / y ]. E! x ph <-> E! x [. Z / y ]. ph )