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 2121 | . 2 |
4 | 1, 3 | eleqtri 2192 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1316 wcel 1465 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 df-clel 2113 |
This theorem is referenced by: 3eltr4i 2199 undifexmid 4087 opi1 4124 opi2 4125 ordpwsucexmid 4455 peano1 4478 acexmidlemcase 5737 acexmidlem2 5739 0lt2o 6306 1lt2o 6307 0elixp 6591 ac6sfi 6760 ctssdccl 6964 exmidomni 6982 infnninf 6990 nnnninf 6991 exmidonfinlem 7017 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 exmidaclem 7032 1lt2pi 7116 prarloclemarch2 7195 prarloclemlt 7269 prarloclemcalc 7278 suplocexprlemdisj 7496 suplocexprlemub 7499 pnfxr 7786 mnfxr 7790 dveflem 12782 |
Copyright terms: Public domain | W3C validator |