|   | 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 4732 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶}) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 {cpr 4627 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-sn 4626 df-pr 4628 | 
| This theorem is referenced by: propeqop 5511 opthwiener 5518 fprg 7174 fprb 7215 fnpr2g 7231 dif1en 9201 dif1enOLD 9203 dfac2b 10172 symg2bas 19411 crctcshwlkn0lem6 29836 wwlksnredwwlkn 29916 wwlksnextprop 29933 clwwlk1loop 30008 clwlkclwwlklem2fv1 30015 clwlkclwwlklem2fv2 30016 clwlkclwwlklem2a 30018 clwlkclwwlklem3 30021 clwwisshclwwslem 30034 clwwlknlbonbgr1 30059 clwwlkn1 30061 frcond1 30286 frgr1v 30291 nfrgr2v 30292 frgr3v 30295 n4cyclfrgr 30311 2clwwlk2clwwlklem 30366 wopprc 43047 mnurndlem1 44305 grtriclwlk3 47917 isubgr3stgrlem4 47941 2arymaptf1 48579 rrx2xpref1o 48644 | 
| Copyright terms: Public domain | W3C validator |