| 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 5145 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | |
| 3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 class class class wbr 5143 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 df-br 5144 |
| This theorem is referenced by: breq123d 5157 breqdi 5158 sbcbr123 5197 sbcbr 5198 sbcbr12g 5199 fvmptopab 7487 fvmptopabOLD 7488 brfvopab 7490 mptmpoopabbrd 8105 mptmpoopabbrdOLD 8106 mptmpoopabovd 8107 mptmpoopabbrdOLDOLD 8108 mptmpoopabovdOLD 8109 bropopvvv 8115 bropfvvvvlem 8116 sprmpod 8249 fprlem1 8325 wfrlem5OLD 8353 supeq123d 9490 frrlem15 9797 fpwwe2lem11 10681 fpwwe2 10683 brtrclfv 15041 dfrtrclrec2 15097 rtrclreclem3 15099 relexpindlem 15102 shftfib 15111 2shfti 15119 prdsval 17500 pwsle 17537 pwsleval 17538 imasleval 17586 issect 17797 isinv 17804 brcic 17842 ciclcl 17846 cicrcl 17847 isfunc 17909 funcres2c 17948 isfull 17957 isfth 17961 fullpropd 17967 fthpropd 17968 elhoma 18077 isposd 18368 pltval 18377 lubfval 18395 glbfval 18408 joinfval 18418 meetfval 18432 odujoin 18453 odumeet 18455 ipole 18579 eqgval 19195 unitpropd 20417 rngcifuestrc 20639 znleval 21573 ltbval 22061 opsrval 22064 lmbr 23266 metustexhalf 24569 metucn 24584 isphtpc 25026 taylthlem1 26415 ulmval 26423 tgjustf 28481 iscgrg 28520 legov 28593 ishlg 28610 opphllem5 28759 opphllem6 28760 hpgbr 28768 iscgra 28817 acopy 28841 isinag 28846 isleag 28855 iseqlg 28875 wlkonprop 29676 wksonproplem 29722 wksonproplemOLD 29723 istrlson 29725 upgrwlkdvspth 29759 ispthson 29762 isspthson 29763 cyclispthon 29824 wspthsn 29868 wspthsnon 29872 iswspthsnon 29876 1pthon2v 30172 3wlkond 30190 dfconngr1 30207 isconngr 30208 isconngr1 30209 1conngr 30213 conngrv2edg 30214 minvecolem4b 30897 minvecolem4 30899 br8d 32622 ressprs 32954 resstos 32957 mntoval 32972 mgcoval 32976 mgcval 32977 isomnd 33078 submomnd 33087 ogrpaddltrd 33096 isinftm 33188 isorng 33329 rprmval 33544 metidv 33891 pstmfval 33895 faeval 34247 brfae 34249 isacycgr 35150 isacycgr1 35151 issconn 35231 satfbrsuc 35371 mclsax 35574 weiunpo 36466 weiunfr 36468 bj-imdirval3 37185 unceq 37604 alrmomodm 38360 relbrcoss 38447 lcvbr 39022 isopos 39181 cmtvalN 39212 isoml 39239 cvrfval 39269 cvrval 39270 pats 39286 isatl 39300 iscvlat 39324 ishlat1 39353 llnset 39507 lplnset 39531 lvolset 39574 lineset 39740 psubspset 39746 pmapfval 39758 lautset 40084 ldilfset 40110 ltrnfset 40119 trlfset 40162 diaffval 41032 dicffval 41176 dihffval 41232 prjspnvs 42630 fnwe2lem2 43063 fnwe2lem3 43064 aomclem8 43073 brfvid 43700 brfvidRP 43701 brfvrcld 43704 brfvrcld2 43705 iunrelexpuztr 43732 brtrclfv2 43740 neicvgnvor 44129 neicvgel1 44132 fperdvper 45934 upwlkbprop 48054 isprsd 48852 lubeldm2d 48855 glbeldm2d 48856 catprsc 48902 catprsc2 48903 prsthinc 49111 prstcle 49159 |
| Copyright terms: Public domain | W3C validator |