Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeltrdi | GIF version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eqeltrdi.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eqeltrdi.2 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
eqeltrdi | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrdi.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | eqeltrdi.2 | . . 3 ⊢ 𝐵 ∈ 𝐶 | |
3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶) |
4 | 1, 3 | eqeltrd 2241 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 ∈ wcel 2135 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: eqeltrrdi 2256 snexprc 4160 onsucelsucexmidlem 4501 dcextest 4553 nnpredcl 4595 ovprc 5869 nnmcl 6441 xpsnen 6779 pw1fin 6868 xpfi 6887 snexxph 6907 ctssdclemn0 7067 nninfisollemne 7087 nninfisol 7089 exmidonfinlem 7141 pw1on 7174 indpi 7275 nq0m0r 7389 genpelxp 7444 un0mulcl 9140 znegcl 9214 zeo 9288 eqreznegel 9544 xnegcl 9760 modqid0 10276 q2txmodxeq0 10310 ser0 10440 expcllem 10457 m1expcl2 10468 nn0ltexp2 10613 bcval 10652 bccl 10670 hashinfom 10681 resqrexlemlo 10945 iserge0 11274 sumrbdclem 11308 fsum3cvg 11309 summodclem3 11311 summodclem2a 11312 fisumss 11323 binom 11415 bcxmas 11420 prodf1 11473 prodrbdclem 11502 fproddccvg 11503 prodmodclem2a 11507 fprodntrivap 11515 prodssdc 11520 fprodssdc 11521 gcdval 11881 gcdcl 11888 lcmcl 11993 pcxnn0cl 12231 pcxcl 12232 pcmptcl 12261 infpnlem2 12279 ssblps 12992 ssbl 12993 xmeter 13003 blssioo 13112 bj-charfun 13550 012of 13736 2o01f 13737 nninfsellemeqinf 13757 nninffeq 13761 trilpolemclim 13776 iswomni0 13791 |
Copyright terms: Public domain | W3C validator |