![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleqtrrd | GIF 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 2183 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
4 | 1, 3 | eleqtrd 2256 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: 3eltr4d 2261 rspc2vd 3125 exmidsssnc 4203 tfrexlem 6334 nnsucuniel 6495 erref 6554 en1uniel 6803 fin0 6884 fin0or 6885 prarloclemarch2 7417 fzopth 10058 fzoss2 10169 fzosubel3 10193 elfzomin 10203 elfzonlteqm1 10207 fzoend 10219 fzofzp1 10224 fzofzp1b 10225 peano2fzor 10229 zmodfzo 10344 frecuzrdg0 10410 frecuzrdgsuc 10411 frecuzrdgdomlem 10414 frecuzrdg0t 10419 frecuzrdgsuctlem 10420 seq3f1olemqsum 10497 bcn2 10739 summodclem2a 11384 fisumss 11395 fsumm1 11419 fisumcom2 11441 prodmodclem2a 11579 fprodm1 11601 fprodcom2fi 11629 ennnfonelemex 12409 ctinfomlemom 12422 mndpropd 12795 grpsubpropd2 12929 subg0 12993 issubg2m 13002 srgpcomp 13126 srgpcompp 13127 srgpcomppsc 13128 ringpropd 13170 mulgass3 13207 lringuplu 13290 aprcotr 13296 lmtopcnp 13643 txopn 13658 blpnfctr 13832 metcnpi 13908 metcnpi2 13909 cncfmpt2fcntop 13978 limcimolemlt 14026 cnplimclemr 14031 limccnp2lem 14038 limccnp2cntop 14039 dvidlemap 14053 dvcnp2cntop 14056 dvcn 14057 dvaddxxbr 14058 dvmulxxbr 14059 dvef 14081 |
Copyright terms: Public domain | W3C validator |