| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > preq1 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.) |
| Ref | Expression |
|---|---|
| preq1 | ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sneq 4636 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
| 2 | 1 | uneq1d 4167 | . 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶})) |
| 3 | df-pr 4629 | . 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶}) | |
| 4 | df-pr 4629 | . 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶}) | |
| 5 | 2, 3, 4 | 3eqtr4g 2802 | 1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
| Copyright terms: Public domain | W3C validator |