![]() |
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 4687 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1523 class class class wbr 4685 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-clel 2647 df-br 4686 |
This theorem is referenced by: breq123d 4699 breqdi 4700 sbcbr123 4739 sbcbr 4740 sbcbr12g 4741 fvmptopab 6739 brfvopab 6742 mptmpt2opabbrd 7293 mptmpt2opabovd 7294 bropopvvv 7300 bropfvvvvlem 7301 sprmpt2d 7395 wfrlem5 7464 supeq123d 8397 fpwwe2lem12 9501 fpwwe2 9503 brtrclfv 13787 dfrtrclrec2 13841 rtrclreclem3 13844 relexpindlem 13847 shftfib 13856 2shfti 13864 prdsval 16162 pwsle 16199 pwsleval 16200 imasleval 16248 issect 16460 isinv 16467 episect 16492 brcic 16505 ciclcl 16509 cicrcl 16510 isfunc 16571 funcres2c 16608 isfull 16617 isfth 16621 fullpropd 16627 fthpropd 16628 elhoma 16729 isposd 17002 pltval 17007 lubfval 17025 glbfval 17038 joinfval 17048 meetfval 17062 odumeet 17187 odujoin 17189 ipole 17205 eqgval 17690 unitpropd 18743 ltbval 19519 opsrval 19522 znleval 19951 lmbr 21110 metustexhalf 22408 metucn 22423 isphtpc 22840 dvef 23788 taylthlem1 24172 ulmval 24179 iscgrg 25452 legov 25525 ishlg 25542 opphllem5 25688 opphllem6 25689 hpgbr 25697 iscgra 25746 acopy 25769 acopyeu 25770 isinag 25774 isleag 25778 iseqlg 25792 wlkonprop 26610 wksonproplem 26657 istrlson 26659 upgrwlkdvspth 26691 ispthson 26694 isspthson 26695 cyclispthon 26752 wspthsn 26797 wspthsnon 26801 iswspthsnon 26806 iswspthsnonOLD 26807 1pthon2v 27131 3wlkond 27149 dfconngr1 27166 isconngr 27167 isconngr1 27168 1conngr 27172 conngrv2edg 27173 minvecolem4b 27862 minvecolem4 27864 br8d 29548 ressprs 29783 resstos 29788 isomnd 29829 submomnd 29838 ogrpaddltrd 29848 isinftm 29863 isorng 29927 metidv 30063 pstmfval 30067 faeval 30437 brfae 30439 issconn 31334 mclsax 31592 frrlem5 31909 unceq 33516 alrmomodm 34264 relbrcoss 34336 lcvbr 34626 isopos 34785 cmtvalN 34816 isoml 34843 cvrfval 34873 cvrval 34874 pats 34890 isatl 34904 iscvlat 34928 ishlat1 34957 llnset 35109 lplnset 35133 lvolset 35176 lineset 35342 psubspset 35348 pmapfval 35360 lautset 35686 ldilfset 35712 ltrnfset 35721 trlfset 35765 diaffval 36636 dicffval 36780 dihffval 36836 fnwe2lem2 37938 fnwe2lem3 37939 aomclem8 37948 brfvid 38296 brfvidRP 38297 brfvrcld 38300 brfvrcld2 38301 iunrelexpuztr 38328 brtrclfv2 38336 neicvgnvor 38731 neicvgel1 38734 fperdvper 40451 upwlkbprop 42044 rngcifuestrc 42322 |
Copyright terms: Public domain | W3C validator |