Theorem axprALT

Description: Alternate proof of axpr . (Contributed by NM, 14-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	axprALT	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )

Proof

Step	Hyp	Ref	Expression
1		zfpair	|- { x , y } e. _V
2	1	isseti	|- E. z z = { x , y }
3		dfcleq	|- ( z = { x , y } <-> A. w ( w e. z <-> w e. { x , y } ) )
4		vex	|- w e. _V
5	4	elpr	|- ( w e. { x , y } <-> ( w = x \/ w = y ) )
6	5	bibi2i	|- ( ( w e. z <-> w e. { x , y } ) <-> ( w e. z <-> ( w = x \/ w = y ) ) )
7		biimpr	|- ( ( w e. z <-> ( w = x \/ w = y ) ) -> ( ( w = x \/ w = y ) -> w e. z ) )
8	6 7	sylbi	|- ( ( w e. z <-> w e. { x , y } ) -> ( ( w = x \/ w = y ) -> w e. z ) )
9	8	alimi	|- ( A. w ( w e. z <-> w e. { x , y } ) -> A. w ( ( w = x \/ w = y ) -> w e. z ) )
10	3 9	sylbi	|- ( z = { x , y } -> A. w ( ( w = x \/ w = y ) -> w e. z ) )
11	2 10	eximii	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )