![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > breqd | Structured version Visualization version Unicode 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 4418 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 df-cleq 2455 df-clel 2458 df-br 4417 |
This theorem is referenced by: breq123d 4430 breqdi 4431 sbcbr123 4468 sbcbr 4469 sbcbr12g 4470 fvmptopab1 6359 brfvopab 6363 bropopvvv 6901 bropfvvvvlem 6902 sprmpt2d 6997 wfrlem5 7066 supeq123d 7990 fpwwe2lem12 9092 fpwwe2 9094 brtrclfv 13115 dfrtrclrec2 13169 rtrclreclem3 13172 relexpindlem 13175 shftfib 13184 2shfti 13192 prdsval 15402 pwsle 15439 pwsleval 15440 imasleval 15496 issect 15707 isinv 15714 episect 15739 brcic 15752 ciclcl 15756 cicrcl 15757 isfunc 15818 funcres2c 15855 isfull 15864 isfth 15868 fullpropd 15874 fthpropd 15875 elhoma 15976 isposd 16250 pltval 16255 lubfval 16273 glbfval 16286 joinfval 16296 meetfval 16310 odumeet 16435 odujoin 16437 ipole 16453 eqgval 16915 unitpropd 17974 ltbval 18744 opsrval 18747 znleval 19174 lmbr 20323 metustexhalf 21620 metucn 21635 isphtpc 22074 dvef 22981 taylthlem1 23377 ulmval 23384 iscgrg 24606 legov 24679 ishlg 24696 opphllem5 24842 opphllem6 24843 hpgbr 24851 iscgra 24900 acopy 24923 acopyeu 24924 isinag 24928 isleag 24932 iseqlg 24946 wlkon 25310 iswlkon 25311 wlkonprop 25312 trls 25315 trlon 25319 istrlon 25320 trlonprop 25321 pths 25345 spths 25346 pthon 25354 ispthon 25355 pthonprop 25356 spthon 25361 isspthon 25362 spthonprp 25364 cyclispthon 25410 dfconngra1 25448 isconngra 25449 isconngra1 25450 1conngra 25452 clwlk 25530 clwlkcompim 25541 is2wlkonot 25640 is2spthonot 25641 2wlkonot 25642 2spthonot 25643 2wlkonot3v 25652 2spthonot3v 25653 iseupa 25742 minvecolem4b 26569 minvecolem4 26571 minvecolem4bOLD 26579 minvecolem4OLD 26581 br8d 28267 ressprs 28465 resstos 28470 isomnd 28513 submomnd 28522 ogrpaddltrd 28532 isinftm 28547 isorng 28611 metidv 28744 pstmfval 28748 faeval 29118 brfae 29120 isscon 29998 mclsax 30256 frrlem5 30567 lcvbr 32632 isopos 32791 cmtvalN 32822 isoml 32849 cvrfval 32879 cvrval 32880 pats 32896 isatl 32910 iscvlat 32934 ishlat1 32963 llnset 33115 lplnset 33139 lvolset 33182 lineset 33348 psubspset 33354 pmapfval 33366 lautset 33692 ldilfset 33718 ltrnfset 33727 trlfset 33771 diaffval 34643 dicffval 34787 dihffval 34843 fnwe2lem2 35954 fnwe2lem3 35955 aomclem8 35964 brfvid 36324 brfvidRP 36325 brfvrcld 36328 brfvrcld2 36329 iunrelexpuztr 36356 brtrclfv2 36364 fperdvper 37828 mptmpt2opabbrd 39076 mptmpt2opabovd 39077 wlkbProp 39680 wlkOnprop 39709 1wlksonproplem 39740 istrlson 39742 upgrwlkdvspth 39771 ispthson 39774 isspthson 39775 cyclisPthon 39823 1pthon2v-av 39868 31wlkond 39912 dfconngr1 39929 isconngr 39930 isconngr1 39931 1conngr 39935 rngcifuestrc 40272 |
Copyright terms: Public domain | W3C validator |