Theorem axc14

Description: Axiom ax-c14 is redundant if we assume ax-5 . Remark 9.6 in Megill p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.

Note that w is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 and ax-5 . By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-Jun-1995) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		hbn1	|- ( -. A. z z = y -> A. z -. A. z z = y )
2		dveel2	|- ( -. A. z z = y -> ( w e. y -> A. z w e. y ) )
3	1 2	hbim1	|- ( ( -. A. z z = y -> w e. y ) -> A. z ( -. A. z z = y -> w e. y ) )
4		elequ1	|- ( w = x -> ( w e. y <-> x e. y ) )
5	4	imbi2d	|- ( w = x -> ( ( -. A. z z = y -> w e. y ) <-> ( -. A. z z = y -> x e. y ) ) )
6	3 5	dvelim	|- ( -. A. z z = x -> ( ( -. A. z z = y -> x e. y ) -> A. z ( -. A. z z = y -> x e. y ) ) )
7		nfa1	|- F/ z A. z z = y
8	7	nfn	|- F/ z -. A. z z = y
9	8	19.21	|- ( A. z ( -. A. z z = y -> x e. y ) <-> ( -. A. z z = y -> A. z x e. y ) )
10	6 9	syl6ib	|- ( -. A. z z = x -> ( ( -. A. z z = y -> x e. y ) -> ( -. A. z z = y -> A. z x e. y ) ) )
11	10	pm2.86d	|- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )