![]() |
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 2210 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)) |
3 | eleq1d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
4 | 3 | eleq1d 2209 | . 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷)) |
5 | 2, 4 | bitrd 187 | 1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1332 ∈ wcel 1481 |
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 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: cbvraldva2 2664 cbvrexdva2 2665 cdeqel 2909 ru 2912 sbcel12g 3022 cbvralcsf 3067 cbvrexcsf 3068 cbvreucsf 3069 cbvrabcsf 3070 onintexmid 4495 elvvuni 4611 elrnmpt1 4798 smoeq 6195 smores 6197 smores2 6199 iordsmo 6202 nnaordi 6412 nnaordr 6414 fvixp 6605 cbvixp 6617 mptelixpg 6636 exmidaclem 7081 cc1 7097 cc2lem 7098 cc3 7100 ltapig 7170 ltmpig 7171 fzsubel 9871 elfzp1b 9908 ennnfonelemg 11952 ennnfonelemp1 11955 ennnfonelemnn0 11971 ctiunctlemu1st 11983 ctiunctlemu2nd 11984 ctiunctlemudc 11986 ctiunctlemfo 11988 istps 12238 tpspropd 12242 eltpsg 12246 isms 12661 mspropd 12686 cnlimci 12850 |
Copyright terms: Public domain | W3C validator |