Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > preq2d | Structured version Visualization version GIF version |
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Ref | Expression |
---|---|
preq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
preq2d | ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | preq2 4662 | . 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 {cpr 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-sn 4558 df-pr 4560 |
This theorem is referenced by: opeq2 4796 opthwiener 5395 fprg 6909 fprb 6948 fnprb 6962 fnpr2g 6964 opthreg 9069 fzosplitprm1 13135 s2prop 14257 gsumprval 17886 indislem 21536 isconn 21949 hmphindis 22333 wilthlem2 25573 ispth 27431 wwlksnredwwlkn 27600 wwlksnextfun 27603 wwlksnextinj 27604 wwlksnextsurj 27605 wwlksnextbij 27607 clwlkclwwlklem2a1 27697 clwlkclwwlklem2a4 27702 clwlkclwwlklem2 27705 clwwisshclwwslemlem 27718 clwwlkn2 27749 clwwlkf 27753 clwwlknonex2lem1 27813 eupth2lem3lem3 27936 eupth2 27945 frcond1 27972 nfrgr2v 27978 frgr3v 27981 n4cyclfrgr 27997 measxun2 31368 altopthsn 33319 mapdindp4 38739 isomuspgrlem2d 43873 rrx2xpref1o 44633 |
Copyright terms: Public domain | W3C validator |