![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleq12d | Unicode 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 2104 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eleq1d.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | eleq1d 2103 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | bitrd 177 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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: cbvraldva2 2531 cbvrexdva2 2532 cdeqel 2754 ru 2757 sbcel12g 2859 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 elvvuni 4347 elrnmpt1 4528 smoeq 5846 smores 5848 smores2 5850 iordsmo 5853 nnaordi 6017 nnaordr 6019 ltapig 6322 ltmpig 6323 fzsubel 8693 elfzp1b 8729 |
Copyright terms: Public domain | W3C validator |