Theorem altopthb

Description: Alternate ordered pair theorem with different sethood requirements. See altopth for more comments. (Contributed by Scott Fenton, 14-Apr-2012)

	Ref	Expression
Hypotheses	altopthb.1	$$⊢A\in \mathrm{V}$$
	altopthb.2	$$⊢D\in \mathrm{V}$$
Assertion	altopthb	$$⊢⟪A,B⟫=⟪C,D⟫\leftrightarrow \left(A=C\wedge B=D\right)$$

Proof

Step	Hyp	Ref	Expression
1		altopthb.1	$$⊢A\in \mathrm{V}$$
2		altopthb.2	$$⊢D\in \mathrm{V}$$
3		altopthbg	$$⊢\left(A\in \mathrm{V}\wedge D\in \mathrm{V}\right)\to \left(⟪A,B⟫=⟪C,D⟫\leftrightarrow \left(A=C\wedge B=D\right)\right)$$
4	1 2 3	mp2an	$$⊢⟪A,B⟫=⟪C,D⟫\leftrightarrow \left(A=C\wedge B=D\right)$$