Theorem prex

Description: The Axiom of Pairing using class variables. Theorem 7.13 of Quine p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

	Ref	Expression
Assertion	prex	|- { A , B } e. _V

Proof

Step	Hyp	Ref	Expression
1		axprg	|- E. z A. w ( ( w = A \/ w = B ) -> w e. z )
2	1	sepexi	|- E. z A. w ( w e. z <-> ( w = A \/ w = B ) )
3		dfcleq	|- ( z = { A , B } <-> A. w ( w e. z <-> w e. { A , B } ) )
4		vex	|- w e. _V
5	4	elpr	|- ( w e. { A , B } <-> ( w = A \/ w = B ) )
6	5	bibi2i	|- ( ( w e. z <-> w e. { A , B } ) <-> ( w e. z <-> ( w = A \/ w = B ) ) )
7	6	albii	|- ( A. w ( w e. z <-> w e. { A , B } ) <-> A. w ( w e. z <-> ( w = A \/ w = B ) ) )
8	3 7	bitri	|- ( z = { A , B } <-> A. w ( w e. z <-> ( w = A \/ w = B ) ) )
9	8	exbii	|- ( E. z z = { A , B } <-> E. z A. w ( w e. z <-> ( w = A \/ w = B ) ) )
10	2 9	mpbir	|- E. z z = { A , B }
11	10	issetri	|- { A , B } e. _V