![]() |
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 4630 | . 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 {cpr 4527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-v 3443 df-un 3886 df-sn 4526 df-pr 4528 |
This theorem is referenced by: opeq2 4765 opeq2OLD 4766 opthwiener 5369 fprg 6894 fprb 6933 fnprb 6948 fnpr2g 6950 opthreg 9065 fzosplitprm1 13142 s2prop 14260 gsumprval 17890 indislem 21605 isconn 22018 hmphindis 22402 wilthlem2 25654 ispth 27512 wwlksnredwwlkn 27681 wwlksnextfun 27684 wwlksnextinj 27685 wwlksnextsurj 27686 wwlksnextbij 27688 clwlkclwwlklem2a1 27777 clwlkclwwlklem2a4 27782 clwlkclwwlklem2 27785 clwwisshclwwslemlem 27798 clwwlkn2 27829 clwwlkf 27832 clwwlknonex2lem1 27892 eupth2lem3lem3 28015 eupth2 28024 frcond1 28051 nfrgr2v 28057 frgr3v 28060 n4cyclfrgr 28076 measxun2 31579 altopthsn 33535 mapdindp4 39019 isomuspgrlem2d 44349 2arymaptf1 45067 rrx2xpref1o 45132 |
Copyright terms: Public domain | W3C validator |