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 4624 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 {cpr 4518 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3848 df-sn 4517 df-pr 4519 |
This theorem is referenced by: propeqop 5364 opthwiener 5371 fprg 6927 fprb 6966 fnpr2g 6983 dif1en 8761 dfac2b 9630 symg2bas 18639 crctcshwlkn0lem6 27753 wwlksnredwwlkn 27833 wwlksnextprop 27850 clwwlk1loop 27925 clwlkclwwlklem2fv1 27932 clwlkclwwlklem2fv2 27933 clwlkclwwlklem2a 27935 clwlkclwwlklem3 27938 clwwisshclwwslem 27951 clwwlknlbonbgr1 27976 clwwlkn1 27978 frcond1 28203 frgr1v 28208 nfrgr2v 28209 frgr3v 28212 n4cyclfrgr 28228 2clwwlk2clwwlklem 28283 wopprc 40444 mnurndlem1 41461 isomuspgrlem2d 44837 2arymaptf1 45553 rrx2xpref1o 45618 |
Copyright terms: Public domain | W3C validator |