Description: Equality of the first members of equal alternate ordered pairs, which holds regardless of the second members' sethood. (Contributed by Scott Fenton, 22-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | altopth1 | ⊢ ( 𝐴 ∈ 𝑉 → ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ → 𝐴 = 𝐶 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | altopthsn | ⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) ) | |
2 | sneqrg | ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐶 } → 𝐴 = 𝐶 ) ) | |
3 | 2 | adantrd | ⊢ ( 𝐴 ∈ 𝑉 → ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) → 𝐴 = 𝐶 ) ) |
4 | 1 3 | syl5bi | ⊢ ( 𝐴 ∈ 𝑉 → ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ → 𝐴 = 𝐶 ) ) |