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