Description: Alternate ordered pair theorem. (Contributed by Scott Fenton, 22-Mar-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | altopthg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | altopthsn | ⊢ ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) ) | |
2 | sneqbg | ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐶 } ↔ 𝐴 = 𝐶 ) ) | |
3 | sneqbg | ⊢ ( 𝐵 ∈ 𝑊 → ( { 𝐵 } = { 𝐷 } ↔ 𝐵 = 𝐷 ) ) | |
4 | 2 3 | bi2anan9 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { 𝐴 } = { 𝐶 } ∧ { 𝐵 } = { 𝐷 } ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) |
5 | 1 4 | syl5bb | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟪ 𝐴 , 𝐵 ⟫ = ⟪ 𝐶 , 𝐷 ⟫ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) |