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	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vz	$$setvarz$$
1		vw	$$setvarw$$
2	1	cv	$$setvarw$$
3		vx	$$setvarx$$
4	3	cv	$$setvarx$$
5	2 4	wceq	$$wffw=x$$
6		vy	$$setvary$$
7	6	cv	$$setvary$$
8	2 7	wceq	$$wffw=y$$
9	5 8	wo	$$wff\left(w=x\vee w=y\right)$$
10	0	cv	$$setvarz$$
11	2 10	wcel	$$wffw\in z$$
12	9 11	wi	$$wff\left(\left(w=x\vee w=y\right)\to w\in z\right)$$
13	12 1	wal	$$wff\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)$$
14	13 0	wex	$$wff\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)$$