Description: Membership in an ordered-pair class abstraction implies membership in a Cartesian product. (Contributed by Alexander van der Vekens, 23-Jun-2018) Avoid ax-sep , ax-nul , ax-pr . (Revised by SN, 11-Dec-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | elopaelxp | ⊢ ( 𝐴 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → 𝐴 ∈ ( V × V ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | ⊢ 𝑥 ∈ V | |
2 | vex | ⊢ 𝑦 ∈ V | |
3 | 1 2 | pm3.2i | ⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) |
4 | 3 | a1i | ⊢ ( 𝜓 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) |
5 | 4 | ssopab2i | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } |
6 | df-xp | ⊢ ( V × V ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } | |
7 | 5 6 | sseqtrri | ⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ⊆ ( V × V ) |
8 | 7 | sseli | ⊢ ( 𝐴 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } → 𝐴 ∈ ( V × V ) ) |