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 2187 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) |
3 | eleq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | eleq1d 2186 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷)) |
5 | 2, 4 | bitrd 187 | 1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1316 ∈ wcel 1465 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 df-clel 2113 |
This theorem is referenced by: cbvraldva2 2635 cbvrexdva2 2636 cdeqel 2878 ru 2881 sbcel12g 2988 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 onintexmid 4457 elvvuni 4573 elrnmpt1 4760 smoeq 6155 smores 6157 smores2 6159 iordsmo 6162 nnaordi 6372 nnaordr 6374 fvixp 6565 cbvixp 6577 mptelixpg 6596 exmidaclem 7032 ltapig 7114 ltmpig 7115 fzsubel 9808 elfzp1b 9845 ennnfonelemg 11843 ennnfonelemp1 11846 ennnfonelemnn0 11862 ctiunctlemu1st 11874 ctiunctlemu2nd 11875 ctiunctlemudc 11877 ctiunctlemfo 11879 istps 12126 tpspropd 12130 eltpsg 12134 isms 12549 mspropd 12574 cnlimci 12738 |
Copyright terms: Public domain | W3C validator |