Metamath Proof Explorer

Theorem sprssspr

Description: The set of all unordered pairs over a given set V is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion sprssspr ⊢ Pairs ⁡ V ⊆ p | ∃ a ∃ b p = a b

Proof

Step Hyp Ref Expression
1 sprval ⊢ V ∈ V → Pairs ⁡ V = p | ∃ a ∈ V ∃ b ∈ V p = a b
2 r2ex ⊢ ∃ a ∈ V ∃ b ∈ V p = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ p = a b
3 simpr ⊢ a ∈ V ∧ b ∈ V ∧ p = a b → p = a b
4 3 2eximi ⊢ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ p = a b → ∃ a ∃ b p = a b
5 2 4 sylbi ⊢ ∃ a ∈ V ∃ b ∈ V p = a b → ∃ a ∃ b p = a b
6 5 ax-gen ⊢ ∀ p ∃ a ∈ V ∃ b ∈ V p = a b → ∃ a ∃ b p = a b
7 6 a1i ⊢ V ∈ V → ∀ p ∃ a ∈ V ∃ b ∈ V p = a b → ∃ a ∃ b p = a b
8 ss2ab ⊢ p | ∃ a ∈ V ∃ b ∈ V p = a b ⊆ p | ∃ a ∃ b p = a b ↔ ∀ p ∃ a ∈ V ∃ b ∈ V p = a b → ∃ a ∃ b p = a b
9 7 8 sylibr ⊢ V ∈ V → p | ∃ a ∈ V ∃ b ∈ V p = a b ⊆ p | ∃ a ∃ b p = a b
10 1 9 eqsstrd ⊢ V ∈ V → Pairs ⁡ V ⊆ p | ∃ a ∃ b p = a b
11 fvprc ⊢ ¬ V ∈ V → Pairs ⁡ V = ∅
12 0ss ⊢ ∅ ⊆ p | ∃ a ∃ b p = a b
13 12 a1i ⊢ ¬ V ∈ V → ∅ ⊆ p | ∃ a ∃ b p = a b
14 11 13 eqsstrd ⊢ ¬ V ∈ V → Pairs ⁡ V ⊆ p | ∃ a ∃ b p = a b
15 10 14 pm2.61i ⊢ Pairs ⁡ V ⊆ p | ∃ a ∃ b p = a b