**Description:** Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012)

Ref | Expression | ||
---|---|---|---|

Assertion | preq12 | ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | preq1 | ⊢ ( 𝐴 = 𝐶 → { 𝐴 , 𝐵 } = { 𝐶 , 𝐵 } ) | |

2 | preq2 | ⊢ ( 𝐵 = 𝐷 → { 𝐶 , 𝐵 } = { 𝐶 , 𝐷 } ) | |

3 | 1 2 | sylan9eq | ⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) |