![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqbrtrrd | Unicode version |
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.) |
Ref | Expression |
---|---|
eqbrtrrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqbrtrrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqbrtrrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqbrtrrd.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eqcomd 2094 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eqbrtrrd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqbrtrd 3871 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-3an 927 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-v 2622 df-un 3004 df-sn 3456 df-pr 3457 df-op 3459 df-br 3852 |
This theorem is referenced by: dftpos4 6042 phpm 6635 unsnfidcex 6684 fisseneq 6696 f1finf1o 6710 prmuloclemcalc 7178 mullocprlem 7183 cauappcvgprlemladdfl 7268 caucvgprlemopl 7282 caucvgprprlemloccalc 7297 caucvgprprlemopl 7310 ltadd1sr 7376 axarch 7480 lemulge11 8381 modqmuladdim 9828 ltexp2a 10061 leexp2a 10062 nnlesq 10112 faclbnd6 10206 facavg 10208 fiprsshashgt1 10279 cvg1nlemcxze 10469 resqrexlemover 10497 resqrexlemlo 10500 resqrexlemnmsq 10504 resqrexlemnm 10505 leabs 10561 abs3dif 10592 abs2dif 10593 maxabslemlub 10694 maxltsup 10705 recn2 10759 imcn2 10760 iserex 10781 isermulc2 10783 isummolem2a 10825 isummulc2 10874 fsumge1 10909 isumrpcl 10942 cvgratnnlemseq 10974 cvgratnnlemsumlt 10976 mertenslemi1 10983 ege2le3 11015 efgt1p2 11039 efgt1p 11040 tanval2ap 11058 tanval3ap 11059 eirraplem 11118 divalglemnqt 11252 mulgcd 11337 dvdssqlem 11351 nn0seqcvgd 11355 mulgcddvds 11408 rpdvds 11413 pw2dvdseulemle 11477 sqrt2irraplemnn 11489 qden1elz 11515 phimullem 11533 hashgcdlem 11535 hashgcdeq 11536 |
Copyright terms: Public domain | W3C validator |