![]() |
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 4692 | . 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵}) | |
2 | preq2 4693 | . 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷}) | |
3 | 1, 2 | sylan9eq 2797 | 1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 {cpr 4586 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-un 3913 df-sn 4585 df-pr 4587 |
This theorem is referenced by: preq12i 4697 preq12d 4700 ssprsseq 4783 preq12b 4806 prnebg 4811 preq12nebg 4818 opthprneg 4820 relop 5804 opthreg 9512 hashle2pr 14330 wwlktovfo 14807 joinval 18226 meetval 18240 ipole 18383 sylow1 19344 frgpuplem 19513 uspgr2wlkeq 28423 wlkres 28447 wlkp1lem8 28457 usgr2pthlem 28540 2wlkdlem10 28709 1wlkdlem4 28913 3wlkdlem6 28938 3wlkdlem10 28942 pfxwlk 33529 oppr 45165 imarnf1pr 45415 elsprel 45568 sprsymrelf1lem 45584 sprsymrelf 45588 paireqne 45604 sbcpr 45614 isomuspgrlem2b 45922 isomuspgrlem2d 45924 |
Copyright terms: Public domain | W3C validator |