![]() |
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 4458 | . 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 {cpr 4370 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-v 3387 df-un 3774 df-sn 4369 df-pr 4371 |
This theorem is referenced by: opeq2 4594 opthwiener 5170 fprg 6650 fnprb 6701 fnpr2g 6703 opthreg 8763 opthregOLD 8765 fzosplitprm1 12833 s2prop 13992 gsumprval 17596 indislem 21133 isconn 21545 hmphindis 21929 wilthlem2 25147 ispth 26977 wwlksnredwwlkn 27165 wwlksnredwwlknOLD 27166 wwlksnextfun 27170 wwlksnextinj 27171 wwlksnextsurj 27172 wwlksnextfunOLD 27175 wwlksnextinjOLD 27176 wwlksnextsurOLD 27177 wwlksnextbij 27179 wwlksnextbijOLD 27180 clwlkclwwlklem2a1 27285 clwlkclwwlklem2a4 27290 clwlkclwwlklem2 27293 clwwisshclwwslemlem 27315 clwwlkn2 27353 clwwlkfOLD 27356 clwwlkf 27361 clwwlknonex2lem1 27447 eupth2lem3lem3 27575 eupth2 27584 frcond1 27615 nfrgr2v 27621 frgr3v 27624 n4cyclfrgr 27640 extwwlkfablem1OLD 27691 measxun2 30789 fprb 32183 altopthsn 32581 mapdindp4 37744 isomuspgrlem2d 42501 |
Copyright terms: Public domain | W3C validator |