Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq12d | GIF version |
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.) |
Ref | Expression |
---|---|
eleq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
eleq12d.2 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
eleq12d | ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq12d.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
2 | 1 | eleq2d 2240 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) |
3 | eleq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | eleq1d 2239 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷)) |
5 | 2, 4 | bitrd 187 | 1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1348 ∈ wcel 2141 |
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 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-4 1503 ax-17 1519 ax-ial 1527 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 df-clel 2166 |
This theorem is referenced by: cbvraldva2 2703 cbvrexdva2 2704 cdeqel 2951 ru 2954 sbcel12g 3064 cbvralcsf 3111 cbvrexcsf 3112 cbvreucsf 3113 cbvrabcsf 3114 onintexmid 4557 elvvuni 4675 elrnmpt1 4862 canth 5807 smoeq 6269 smores 6271 smores2 6273 iordsmo 6276 nnaordi 6487 nnaordr 6489 fvixp 6681 cbvixp 6693 mptelixpg 6712 exmidaclem 7185 cc1 7227 cc2lem 7228 cc3 7230 ltapig 7300 ltmpig 7301 fzsubel 10016 elfzp1b 10053 ennnfonelemg 12358 ennnfonelemp1 12361 ennnfonelemnn0 12377 ctiunctlemu1st 12389 ctiunctlemu2nd 12390 ctiunctlemudc 12392 ctiunctlemfo 12394 ismgm 12611 mgm1 12624 ismndd 12673 istps 12824 tpspropd 12828 eltpsg 12832 isms 13247 mspropd 13272 cnlimci 13436 |
Copyright terms: Public domain | W3C validator |