![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrrd | Unicode version |
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
eleqtrrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eleqtrrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eleqtrrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrrd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eleqtrrd.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | eqcomd 2042 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eleqtrd 2113 |
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 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: 3eltr4d 2118 tfrexlem 5889 erref 6062 en1uniel 6220 prarloclemarch2 6402 fzopth 8694 fzoss2 8798 fzosubel3 8822 elfzomin 8832 elfzonlteqm1 8836 fzoend 8848 fzofzp1 8853 fzofzp1b 8854 peano2fzor 8858 frecuzrdgcl 8880 frecuzrdg0 8881 frecuzrdgsuc 8882 |
Copyright terms: Public domain | W3C validator |