![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqbrtrrd | GIF 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 2105 | . 2 ⊢ (𝜑 → 𝐵 = 𝐴) |
3 | eqbrtrrd.2 | . 2 ⊢ (𝜑 → 𝐴𝑅𝐶) | |
4 | 2, 3 | eqbrtrd 3895 | 1 ⊢ (𝜑 → 𝐵𝑅𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1299 class class class wbr 3875 |
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 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-un 3025 df-sn 3480 df-pr 3481 df-op 3483 df-br 3876 |
This theorem is referenced by: dftpos4 6090 phpm 6688 unsnfidcex 6737 fisseneq 6749 f1finf1o 6763 prmuloclemcalc 7274 mullocprlem 7279 cauappcvgprlemladdfl 7364 caucvgprlemopl 7378 caucvgprprlemloccalc 7393 caucvgprprlemopl 7406 ltadd1sr 7472 axarch 7576 lemulge11 8482 xaddge0 9502 modqmuladdim 9981 ltexp2a 10186 leexp2a 10187 nnlesq 10237 faclbnd6 10331 facavg 10333 fiprsshashgt1 10404 cvg1nlemcxze 10594 resqrexlemover 10622 resqrexlemlo 10625 resqrexlemnmsq 10629 resqrexlemnm 10630 leabs 10686 abs3dif 10717 abs2dif 10718 maxabslemlub 10819 maxltsup 10830 bdtri 10850 xrmaxiflemab 10855 xrbdtri 10884 recn2 10925 imcn2 10926 iserex 10947 summodclem2a 10989 fsumge1 11069 isumrpcl 11102 cvgratnnlemseq 11134 cvgratnnlemsumlt 11136 mertenslemi1 11143 ege2le3 11175 efgt1p2 11199 efgt1p 11200 tanval2ap 11218 tanval3ap 11219 eirraplem 11278 divalglemnqt 11412 mulgcd 11497 dvdssqlem 11511 nn0seqcvgd 11515 mulgcddvds 11568 rpdvds 11573 pw2dvdseulemle 11637 sqrt2irraplemnn 11649 qden1elz 11675 phimullem 11693 hashgcdlem 11695 hashgcdeq 11696 ennnfonelemex 11719 lmcn2 12230 psmetge0 12259 xmetge0 12293 |
Copyright terms: Public domain | W3C validator |