Metamath Proof Explorer

Theorem sprid

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

Ref Expression
Assertion sprid ⊢ p | ∃ a ∈ V ∃ b ∈ V p = a b = p | ∃ a ∃ b p = a b

Proof

Step Hyp Ref Expression
1 rexv ⊢ ∃ a ∈ V ∃ b ∈ V p = a b ↔ ∃ a ∃ b ∈ V p = a b
2 rexv ⊢ ∃ b ∈ V p = a b ↔ ∃ b p = a b
3 2 exbii ⊢ ∃ a ∃ b ∈ V p = a b ↔ ∃ a ∃ b p = a b
4 1 3 bitri ⊢ ∃ a ∈ V ∃ b ∈ V p = a b ↔ ∃ a ∃ b p = a b
5 4 abbii ⊢ p | ∃ a ∈ V ∃ b ∈ V p = a b = p | ∃ a ∃ b p = a b