Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq2i | GIF version |
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eleq2i | ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | eleq2 2101 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1243 ∈ wcel 1393 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 |
This theorem is referenced by: eleq12i 2105 eleqtri 2112 eleq2s 2132 hbxfreq 2144 abeq2i 2148 abeq1i 2149 nfceqi 2174 raleqbii 2336 rexeqbii 2337 rabeq2i 2554 elab2g 2689 elrabf 2696 elrab3t 2697 elrab2 2700 cbvsbc 2791 elin2 3127 dfnul2 3226 noel 3228 rabn0m 3245 rabeq0 3247 eltpg 3416 tpid3g 3483 oprcl 3573 elunirab 3593 elintrab 3627 exss 3963 elop 3968 opm 3971 brabsb 3998 brabga 4001 pofun 4049 elsuci 4140 elsucg 4141 elsuc2g 4142 ordsucim 4226 peano2 4318 elxp 4362 brab2a 4393 brab2ga 4415 elcnv 4512 dmmrnm 4554 elrnmptg 4586 opelres 4617 rninxp 4764 funco 4940 elfv 5176 nfvres 5206 fvopab3g 5245 fvmptssdm 5255 fmptco 5330 funfvima 5390 fliftel 5433 acexmidlema 5503 acexmidlemb 5504 acexmidlem2 5509 eloprabga 5591 elrnmpt2 5614 ovid 5617 offval 5719 xporderlem 5852 brtpos2 5866 issmo 5903 smores3 5908 tfrlem7 5933 tfrlem9 5935 tfr0 5937 tfri2 5952 el1o 6020 dif1o 6021 elecg 6144 brecop 6196 erovlem 6198 oviec 6212 isfi 6241 enssdom 6242 xpcomco 6300 elni 6406 nlt1pig 6439 0nnq 6462 dfmq0qs 6527 dfplq0qs 6528 nqnq0 6539 elinp 6572 0npr 6581 ltdfpr 6604 nqprl 6649 nqpru 6650 addnqprlemfl 6657 addnqprlemfu 6658 mulnqprlemfl 6673 mulnqprlemfu 6674 cauappcvgprlemladdru 6754 addsrpr 6830 mulsrpr 6831 opelcn 6903 opelreal 6904 elreal 6905 elreal2 6907 0ncn 6908 addcnsr 6910 mulcnsr 6911 addvalex 6920 peano1nnnn 6928 peano2nnnn 6929 xrlenlt 7084 1nn 7925 peano2nn 7926 elnn0 8183 elnnne0 8195 un0addcl 8215 un0mulcl 8216 uztrn2 8490 elnnuz 8509 elnn0uz 8510 elq 8557 elxr 8696 elfzm1b 8960 frecfzennn 9203 iseqf 9224 iser0 9250 iser0f 9251 clim2iser 9857 clim2iser2 9858 iisermulc2 9860 iserile 9862 climserile 9865 ialgrlemconst 9882 ialgrf 9884 bdceq 9962 bj-nntrans 10076 bj-nnelirr 10078 |
Copyright terms: Public domain | W3C validator |