Theorem sprid

Description: Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021)

	Ref	Expression
Assertion	sprid	⊢ { 𝑝 ∣ ∃ 𝑎 ∈ V ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }

Proof

Step	Hyp	Ref	Expression
1		rexv	⊢ ( ∃ 𝑎 ∈ V ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } )
2		rexv	⊢ ( ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
3	2	exbii	⊢ ( ∃ 𝑎 ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
4	1 3	bitri	⊢ ( ∃ 𝑎 ∈ V ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } ↔ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } )
5	4	abbii	⊢ { 𝑝 ∣ ∃ 𝑎 ∈ V ∃ 𝑏 ∈ V 𝑝 = { 𝑎 , 𝑏 } } = { 𝑝 ∣ ∃ 𝑎 ∃ 𝑏 𝑝 = { 𝑎 , 𝑏 } }