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	⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		oppr	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
2	1	el2v	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
3	2	eqcomd	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
4	3	eqcoms	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
5	4	anim1i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )
6	5	2eximi	⊢ ( ∃ 𝑎 ∃ 𝑏 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝜑 ) → ∃ 𝑎 ∃ 𝑏 ( { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ∧ 𝜑 ) )