![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrri | Unicode version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleqtrr.1 |
![]() ![]() ![]() ![]() |
eleqtrr.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eleqtrri |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleqtrr.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | eleqtrr.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | eqcomi 2089 |
. 2
![]() ![]() ![]() ![]() |
4 | 1, 3 | eleqtri 2159 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1379 ax-gen 1381 ax-ie1 1425 ax-ie2 1426 ax-4 1443 ax-17 1462 ax-ial 1470 ax-ext 2067 |
This theorem depends on definitions: df-bi 115 df-cleq 2078 df-clel 2081 |
This theorem is referenced by: 3eltr4i 2166 undifexmid 3995 opi1 4026 opi2 4027 ordpwsucexmid 4352 peano1 4375 acexmidlemcase 5589 acexmidlem2 5591 ac6sfi 6547 djuun 6681 exmidomni 6719 fodjuomnilemf 6721 infnninf 6726 nnnninf 6727 exmidfodomrlemr 6749 exmidfodomrlemrALT 6750 1lt2pi 6820 prarloclemarch2 6899 prarloclemlt 6973 prarloclemcalc 6982 pnfxr 7461 mnfxr 7465 0lt2o 11242 1lt2o 11243 |
Copyright terms: Public domain | W3C validator |