Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqeltrid | GIF version |
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eqeltrid.1 | ⊢ 𝐴 = 𝐵 |
eqeltrid.2 | ⊢ (𝜑 → 𝐵 ∈ 𝐶) |
Ref | Expression |
---|---|
eqeltrid | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrid.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
3 | eqeltrid.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶) | |
4 | 2, 3 | eqeltrd 2216 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∈ wcel 1480 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 |
This theorem is referenced by: eqeltrrid 2227 csbexga 4056 otexg 4152 tpexg 4365 dmresexg 4842 f1oabexg 5379 funfvex 5438 riotaexg 5734 riotaprop 5753 fnovex 5804 ovexg 5805 fovrn 5913 fnovrn 5918 cofunexg 6009 cofunex2g 6010 abrexex2g 6018 xpexgALT 6031 mpofvex 6101 tfrex 6265 frec0g 6294 freccllem 6299 ecexg 6433 qsexg 6485 pmex 6547 elixpsn 6629 diffifi 6788 unfidisj 6810 prfidisj 6815 tpfidisj 6816 ssfirab 6822 ssfidc 6823 fnfi 6825 funrnfi 6830 iunfidisj 6834 infclti 6910 djuex 6928 ctssdccl 6996 addvalex 7652 negcl 7962 intqfrac2 10092 intfracq 10093 frec2uzzd 10173 frecuzrdgrrn 10181 iseqf1olemqpcl 10269 seq3f1olemqsum 10273 bcval5 10509 xrmaxiflemval 11019 climmpt 11069 reccn2ap 11082 zsumdc 11153 fsumzcl2 11174 fsump1i 11202 fsumabs 11234 hash2iun1dif1 11249 mertenslemi1 11304 algrf 11726 algcvg 11729 algcvga 11732 algfx 11733 eucalgcvga 11739 eucalg 11740 crth 11900 phimullem 11901 ennnfonelemj0 11914 ennnfonelemom 11921 ressid 12020 1strbas 12058 2strbasg 12060 2stropg 12061 restid 12131 topnvalg 12132 topnidg 12133 topopn 12175 topcld 12278 uncld 12282 iuncld 12284 unicld 12285 tgrest 12338 restin 12345 cnco 12390 cnrest 12404 cnptoprest2 12409 lmss 12415 txbasval 12436 txcn 12444 cnmpt12f 12455 hmeoco 12485 idhmeo 12486 blres 12603 metrest 12675 qtopbasss 12690 tgqioo 12716 divcnap 12724 fsumcncntop 12725 cncfmet 12748 cdivcncfap 12756 cnrehmeocntop 12762 cnplimcim 12805 limccnpcntop 12813 limccnp2lem 12814 limccnp2cntop 12815 dvfvalap 12819 bj-snexg 13110 trilpolemcl 13230 |
Copyright terms: Public domain | W3C validator |