![]() |
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 | ⊢ A = B |
Ref | Expression |
---|---|
eleq2i | ⊢ (𝐶 ∈ A ↔ 𝐶 ∈ B) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1i.1 | . 2 ⊢ A = B | |
2 | eleq2 2098 | . 2 ⊢ (A = B → (𝐶 ∈ A ↔ 𝐶 ∈ B)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐶 ∈ A ↔ 𝐶 ∈ B) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1242 ∈ wcel 1390 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: eleq12i 2102 eleqtri 2109 eleq2s 2129 hbxfreq 2141 abeq2i 2145 abeq1i 2146 nfceqi 2171 raleqbii 2330 rexeqbii 2331 rabeq2i 2548 elab2g 2683 elrabf 2690 elrab3t 2691 elrab2 2694 cbvsbc 2785 elin2 3121 dfnul2 3220 noel 3222 rabn0m 3239 rabeq0 3241 eltpg 3407 tpid3g 3474 oprcl 3564 elunirab 3584 elintrab 3618 exss 3954 elop 3959 opm 3962 brabsb 3989 brabga 3992 pofun 4040 elsuci 4106 elsucg 4107 elsuc2g 4108 ordsucim 4192 peano2 4261 elxp 4305 brab2a 4336 brab2ga 4358 elcnv 4455 dmmrnm 4497 elrnmptg 4529 opelres 4560 rninxp 4707 funco 4883 elfv 5119 nfvres 5149 fvopab3g 5188 fvmptssdm 5198 fmptco 5273 funfvima 5333 fliftel 5376 acexmidlema 5446 acexmidlemb 5447 acexmidlem2 5452 eloprabga 5533 elrnmpt2 5556 ovid 5559 offval 5661 xporderlem 5793 brtpos2 5807 issmo 5844 smores3 5849 tfrlem7 5874 tfrlem9 5876 tfr0 5878 tfri2 5893 el1o 5959 dif1o 5960 elecg 6080 brecop 6132 erovlem 6134 oviec 6148 isfi 6177 enssdom 6178 xpcomco 6236 elni 6292 nlt1pig 6325 0nnq 6348 dfmq0qs 6412 dfplq0qs 6413 nqnq0 6424 elinp 6457 0npr 6466 ltdfpr 6489 nqprl 6533 addnqprlemfl 6540 addnqprlemfu 6541 cauappcvgprlemladdru 6628 addsrpr 6673 mulsrpr 6674 opelcn 6725 opelreal 6726 elreal 6727 elreal2 6728 0ncn 6729 addcnsr 6731 mulcnsr 6732 xrlenlt 6881 1nn 7706 peano2nn 7707 elnn0 7959 elnnne0 7971 un0addcl 7991 un0mulcl 7992 uztrn2 8266 elnnuz 8285 elnn0uz 8286 elq 8333 elxr 8466 elfzm1b 8730 frecfzennn 8884 bdceq 9297 bj-nntrans 9411 bj-nnelirr 9413 |
Copyright terms: Public domain | W3C validator |