![]() |
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 4405 | . 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1631 {cpr 4318 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-un 3728 df-sn 4317 df-pr 4319 |
This theorem is referenced by: opeq2 4540 opthwiener 5107 fprg 6565 fnprb 6616 fnpr2g 6618 opthreg 8677 opthregOLD 8679 fzosplitprm1 12786 s2prop 13861 gsumprval 17489 indislem 21025 isconn 21437 hmphindis 21821 wilthlem2 25016 ispth 26854 wwlksnredwwlkn 27039 wwlksnextfun 27042 wwlksnextinj 27043 wwlksnextsur 27044 wwlksnextbij 27046 clwlkclwwlklem2a1 27142 clwlkclwwlklem2a4 27147 clwlkclwwlklem2 27150 clwwisshclwwslemlem 27163 clwwlkn2 27200 clwwlkf 27203 clwwlknonex2lem1 27283 eupth2lem3lem3 27410 eupth2 27419 frcond1 27448 nfrgr2v 27454 frgr3v 27457 n4cyclfrgr 27473 extwwlkfablem1OLD 27524 measxun2 30613 fprb 32007 altopthsn 32405 mapdindp4 37533 |
Copyright terms: Public domain | W3C validator |