![]() |
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 2158 | . 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1296 ∈ wcel 1445 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-4 1452 ax-17 1471 ax-ial 1479 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-cleq 2088 df-clel 2091 |
This theorem is referenced by: eleq12i 2162 eleqtri 2169 eleq2s 2189 hbxfreq 2201 abeq2i 2205 abeq1i 2206 nfceqi 2231 raleqbii 2401 rexeqbii 2402 rabeq2i 2630 elab2g 2776 elrabf 2783 elrab3t 2784 elrab2 2788 cbvsbc 2881 elin2 3203 dfnul2 3304 noel 3306 rabn0m 3329 rabeq0 3331 eltpg 3508 tpid3g 3577 oprcl 3668 elunirab 3688 elintrab 3722 exss 4078 elop 4082 opm 4085 brabsb 4112 brabga 4115 pofun 4163 elsuci 4254 elsucg 4255 elsuc2g 4256 ordsucim 4345 peano2 4438 elxp 4484 brab2a 4520 brab2ga 4542 elco 4633 elcnv 4644 dmmrnm 4686 elrnmptg 4719 opelres 4750 rninxp 4908 funco 5088 elfv 5338 nfvres 5372 fvopab3g 5412 fvmptssdm 5423 fmptco 5503 funfvima 5565 fliftel 5610 acexmidlema 5681 acexmidlemb 5682 acexmidlem2 5687 eloprabga 5773 elrnmpt2 5796 ovid 5799 offval 5901 xporderlem 6034 brtpos2 6054 issmo 6091 smores3 6096 tfrlem7 6120 tfrlem9 6122 tfr0dm 6125 tfri2 6169 rdgon 6189 freccllem 6205 frecfcllem 6207 frecsuclem 6209 el1o 6239 dif1o 6240 nnsucuniel 6296 elecg 6370 brecop 6422 erovlem 6424 oviec 6438 mapsncnv 6492 mptelixpg 6531 isfi 6558 enssdom 6559 map1 6609 xpcomco 6622 exmidpw 6704 fnfi 6726 fidcenumlemrks 6742 fidcenumlemrk 6743 djulclb 6827 djur 6837 eldju 6839 eldju2ndl 6843 eldju2ndr 6844 elni 6964 nlt1pig 6997 0nnq 7020 dfmq0qs 7085 dfplq0qs 7086 nqnq0 7097 elinp 7130 0npr 7139 ltdfpr 7162 nqprl 7207 nqpru 7208 addnqprlemfl 7215 addnqprlemfu 7216 mulnqprlemfl 7231 mulnqprlemfu 7232 cauappcvgprlemladdru 7312 addsrpr 7388 mulsrpr 7389 opelcn 7461 opelreal 7462 elreal 7463 elreal2 7465 0ncn 7466 addcnsr 7468 mulcnsr 7469 addvalex 7478 peano1nnnn 7486 peano2nnnn 7487 xrlenlt 7648 1nn 8531 peano2nn 8532 elnn0 8773 elnnne0 8785 un0addcl 8804 un0mulcl 8805 elxnn0 8836 uztrn2 9135 elnnuz 9154 elnn0uz 9155 elq 9206 elxr 9346 elfzm1b 9661 fz01or 9674 frecfzennn 9982 inftonninf 9996 iseqfcl 10024 iseqfclt 10025 seqf 10026 ser0 10080 ser0f 10081 hashinfom 10317 clim2ser 10895 clim2ser2 10896 isermulc2 10898 iserle 10900 climserle 10903 fsum3cvg3 10954 isumclim3 10981 isumadd 10989 sumsplitdc 10990 iserabs 11033 cvgcmpub 11034 isumshft 11048 isumsplit 11049 isumlessdc 11054 cvgratz 11090 cvgratgt0 11091 divides 11240 dvdsflip 11294 infssuzex 11387 ialgrlemconst 11467 istps 11897 lmss 12112 bdceq 12445 bj-nntrans 12558 bj-nnelirr 12560 ss1oel2o 12598 |
Copyright terms: Public domain | W3C validator |