| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > preq12 | Structured version Visualization version GIF version | ||
| Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
| Ref | Expression |
|---|---|
| preq12 | ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | preq1 4733 | . 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵}) | |
| 2 | preq2 4734 | . 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷}) | |
| 3 | 1, 2 | sylan9eq 2797 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 {cpr 4628 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-sn 4627 df-pr 4629 |
| This theorem is referenced by: preq12i 4738 preq12d 4741 ssprsseq 4825 preq12b 4850 prnebg 4856 preq12nebg 4863 opthprneg 4865 elpr2elpr 4869 relop 5861 opthreg 9658 hashle2pr 14516 wwlktovfo 14997 joinval 18422 meetval 18436 ipole 18579 sylow1 19621 frgpuplem 19790 uspgr2wlkeq 29664 wlkres 29688 wlkp1lem8 29698 usgr2pthlem 29783 2wlkdlem10 29955 1wlkdlem4 30159 3wlkdlem6 30184 3wlkdlem10 30188 pfxwlk 35129 oppr 47042 imarnf1pr 47294 elsprel 47462 sprsymrelf1lem 47478 sprsymrelf 47482 paireqne 47498 sbcpr 47508 isuspgrimlem 47874 grtrif1o 47909 |
| Copyright terms: Public domain | W3C validator |