Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > breqd | Structured version Visualization version GIF version |
Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.) |
Ref | Expression |
---|---|
breq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
breqd | ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | breq 5059 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 class class class wbr 5057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 df-br 5058 |
This theorem is referenced by: breq123d 5071 breqdi 5072 sbcbr123 5111 sbcbr 5112 sbcbr12g 5113 fvmptopab 7198 brfvopab 7200 mptmpoopabbrd 7767 mptmpoopabovd 7768 bropopvvv 7774 bropfvvvvlem 7775 sprmpod 7879 wfrlem5 7948 supeq123d 8902 fpwwe2lem12 10051 fpwwe2 10053 brtrclfv 14350 dfrtrclrec2 14404 rtrclreclem3 14407 relexpindlem 14410 shftfib 14419 2shfti 14427 prdsval 16716 pwsle 16753 pwsleval 16754 imasleval 16802 issect 17011 isinv 17018 brcic 17056 ciclcl 17060 cicrcl 17061 isfunc 17122 funcres2c 17159 isfull 17168 isfth 17172 fullpropd 17178 fthpropd 17179 elhoma 17280 isposd 17553 pltval 17558 lubfval 17576 glbfval 17589 joinfval 17599 meetfval 17613 odumeet 17738 odujoin 17740 ipole 17756 eqgval 18267 unitpropd 19376 ltbval 20180 opsrval 20183 znleval 20629 lmbr 21794 metustexhalf 23093 metucn 23108 isphtpc 23525 taylthlem1 24888 ulmval 24895 tgjustf 26186 iscgrg 26225 legov 26298 ishlg 26315 opphllem5 26464 opphllem6 26465 hpgbr 26473 iscgra 26522 acopy 26546 isinag 26551 isleag 26560 iseqlg 26580 wlkonprop 27367 wksonproplem 27413 istrlson 27415 upgrwlkdvspth 27447 ispthson 27450 isspthson 27451 cyclispthon 27509 wspthsn 27553 wspthsnon 27557 iswspthsnon 27561 1pthon2v 27859 3wlkond 27877 dfconngr1 27894 isconngr 27895 isconngr1 27896 1conngr 27900 conngrv2edg 27901 minvecolem4b 28582 minvecolem4 28584 br8d 30289 ressprs 30569 resstos 30574 isomnd 30629 submomnd 30638 ogrpaddltrd 30647 isinftm 30737 isorng 30799 metidv 31031 pstmfval 31035 faeval 31404 brfae 31406 isacycgr 32289 isacycgr1 32290 issconn 32370 satfbrsuc 32510 mclsax 32713 fprlem1 33034 frrlem15 33039 bj-imdirval3 34366 unceq 34750 alrmomodm 35494 relbrcoss 35566 lcvbr 36037 isopos 36196 cmtvalN 36227 isoml 36254 cvrfval 36284 cvrval 36285 pats 36301 isatl 36315 iscvlat 36339 ishlat1 36368 llnset 36521 lplnset 36545 lvolset 36588 lineset 36754 psubspset 36760 pmapfval 36772 lautset 37098 ldilfset 37124 ltrnfset 37133 trlfset 37176 diaffval 38046 dicffval 38190 dihffval 38246 fnwe2lem2 39529 fnwe2lem3 39530 aomclem8 39539 brfvid 39910 brfvidRP 39911 brfvrcld 39914 brfvrcld2 39915 iunrelexpuztr 39942 brtrclfv2 39950 neicvgnvor 40344 neicvgel1 40347 fperdvper 42079 upwlkbprop 43890 rngcifuestrc 44196 |
Copyright terms: Public domain | W3C validator |