Axiom ax-pr

Description: The Axiom of Pairing of ZF set theory. It was derived as Theorem axpr above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 14-Nov-2006)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vz	|- z
1		vw	|- w
2	1	cv	|- w
3		vx	|- x
4	3	cv	|- x
5	2 4	wceq	|- w = x
6		vy	|- y
7	6	cv	|- y
8	2 7	wceq	|- w = y
9	5 8	wo	|- ( w = x \/ w = y )
10	0	cv	|- z
11	2 10	wcel	|- w e. z
12	9 11	wi	|- ( ( w = x \/ w = y ) -> w e. z )
13	12 1	wal	|- A. w ( ( w = x \/ w = y ) -> w e. z )
14	13 0	wex	|- E. z A. w ( ( w = x \/ w = y ) -> w e. z )