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 4626 | . 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 {cpr 4519 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3849 df-sn 4518 df-pr 4520 |
This theorem is referenced by: opeq2 4762 opeq2OLD 4763 opthwiener 5372 fprg 6928 fprb 6967 fnprb 6982 fnpr2g 6984 opthreg 9155 fzosplitprm1 13239 s2prop 14359 gsumprval 18015 indislem 21752 isconn 22165 hmphindis 22549 wilthlem2 25806 ispth 27664 wwlksnredwwlkn 27833 wwlksnextfun 27836 wwlksnextinj 27837 wwlksnextsurj 27838 wwlksnextbij 27840 clwlkclwwlklem2a1 27929 clwlkclwwlklem2a4 27934 clwlkclwwlklem2 27937 clwwisshclwwslemlem 27950 clwwlkn2 27981 clwwlkf 27984 clwwlknonex2lem1 28044 eupth2lem3lem3 28167 eupth2 28176 frcond1 28203 nfrgr2v 28209 frgr3v 28212 n4cyclfrgr 28228 measxun2 31748 altopthsn 33901 mapdindp4 39357 isomuspgrlem2d 44809 2arymaptf1 45525 rrx2xpref1o 45590 |
Copyright terms: Public domain | W3C validator |