Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > preq1d | Structured version Visualization version GIF version |
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Ref | Expression |
---|---|
preq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
preq1d | ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | preq1 4661 | . 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: propeqop 5388 opthwiener 5395 fprg 6909 fprb 6948 fnpr2g 6964 dfac2b 9544 symg2bas 18455 crctcshwlkn0lem6 27520 wwlksnredwwlkn 27600 wwlksnextprop 27618 clwwlk1loop 27693 clwlkclwwlklem2fv1 27700 clwlkclwwlklem2fv2 27701 clwlkclwwlklem2a 27703 clwlkclwwlklem3 27706 clwwisshclwwslem 27719 clwwlknlbonbgr1 27744 clwwlkn1 27746 frcond1 27972 frgr1v 27977 nfrgr2v 27978 frgr3v 27981 n4cyclfrgr 27997 2clwwlk2clwwlklem 28052 wopprc 39505 mnurndlem1 40494 isomuspgrlem2d 43873 rrx2xpref1o 44633 |
Copyright terms: Public domain | W3C validator |