Theorem 2exopprim

Description: The existence of an ordered pair fulfilling a wff implies the existence of an unordered pair fulfilling the wff. (Contributed by AV, 29-Jul-2023)

	Ref	Expression
Assertion	2exopprim	$$⊢\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		oppr	$$⊢\left(a\in \mathrm{V}\wedge b\in \mathrm{V}\right)\to \left(⟨a,b⟩=⟨A,B⟩\to \left\{a,b\right\}=\left\{A,B\right\}\right)$$
2	1	el2v	$$⊢⟨a,b⟩=⟨A,B⟩\to \left\{a,b\right\}=\left\{A,B\right\}$$
3	2	eqcomd	$$⊢⟨a,b⟩=⟨A,B⟩\to \left\{A,B\right\}=\left\{a,b\right\}$$
4	3	eqcoms	$$⊢⟨A,B⟩=⟨a,b⟩\to \left\{A,B\right\}=\left\{a,b\right\}$$
5	4	anim1i	$$⊢\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)$$
6	5	2eximi	$$⊢\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\to \exists a\exists b\left(\left\{A,B\right\}=\left\{a,b\right\}\wedge \phi \right)$$