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 4555 elvvuni 4673 elrnmpt1 4860 canth 5804 smoeq 6266 smores 6268 smores2 6270 iordsmo 6273 nnaordi 6484 nnaordr 6486 fvixp 6677 cbvixp 6689 mptelixpg 6708 exmidaclem 7172 cc1 7214 cc2lem 7215 cc3 7217 ltapig 7287 ltmpig 7288 fzsubel 10003 elfzp1b 10040 ennnfonelemg 12345 ennnfonelemp1 12348 ennnfonelemnn0 12364 ctiunctlemu1st 12376 ctiunctlemu2nd 12377 ctiunctlemudc 12379 ctiunctlemfo 12381 ismgm 12598 mgm1 12611 ismndd 12660 istps 12783 tpspropd 12787 eltpsg 12791 isms 13206 mspropd 13231 cnlimci 13395 |
Copyright terms: Public domain | W3C validator |