Theorem dveel2ALT

Description: Alternate proof of dveel2 using ax-c16 instead of ax-5 . (Contributed by NM, 10-May-2008) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	dveel2ALT	|- ( -. A. x x = y -> ( z e. y -> A. x z e. y ) )

Proof

Step	Hyp	Ref	Expression
1		ax5el	|- ( z e. w -> A. x z e. w )
2		ax5el	|- ( z e. y -> A. w z e. y )
3		elequ2	|- ( w = y -> ( z e. w <-> z e. y ) )
4	1 2 3	dvelimh	|- ( -. A. x x = y -> ( z e. y -> A. x z e. y ) )