|   | 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 4733 | . 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: opeq2 4873 opthwiener 5518 fprg 7174 fprb 7215 fnprb 7229 fnpr2g 7231 opthreg 9659 fzosplitprm1 13817 s2prop 14947 gsumprval 18702 indislem 23008 isconn 23422 hmphindis 23806 wilthlem2 27113 ispth 29742 wwlksnredwwlkn 29916 wwlksnextfun 29919 wwlksnextinj 29920 wwlksnextsurj 29921 wwlksnextbij 29923 clwlkclwwlklem2a1 30012 clwlkclwwlklem2a4 30017 clwlkclwwlklem2 30020 clwwisshclwwslemlem 30033 clwwlkn2 30064 clwwlkf 30067 clwwlknonex2lem1 30127 eupth2lem3lem3 30250 eupth2 30259 frcond1 30286 nfrgr2v 30292 frgr3v 30295 n4cyclfrgr 30311 measxun2 34212 altopthsn 35963 mapdindp4 41726 clnbgrgrimlem 47906 gpgov 48006 gpg3kgrtriexlem6 48049 2arymaptf1 48579 rrx2xpref1o 48644 | 
| Copyright terms: Public domain | W3C validator |