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	|- ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) -> E. a E. b ( { A , B } = { a , b } /\ ph ) )

Proof

Step	Hyp	Ref	Expression
1		oppr	|- ( ( a e. _V /\ b e. _V ) -> ( <. a , b >. = <. A , B >. -> { a , b } = { A , B } ) )
2	1	el2v	|- ( <. a , b >. = <. A , B >. -> { a , b } = { A , B } )
3	2	eqcomd	|- ( <. a , b >. = <. A , B >. -> { A , B } = { a , b } )
4	3	eqcoms	|- ( <. A , B >. = <. a , b >. -> { A , B } = { a , b } )
5	4	anim1i	|- ( ( <. A , B >. = <. a , b >. /\ ph ) -> ( { A , B } = { a , b } /\ ph ) )
6	5	2eximi	|- ( E. a E. b ( <. A , B >. = <. a , b >. /\ ph ) -> E. a E. b ( { A , B } = { a , b } /\ ph ) )