Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq1i | Unicode version |
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleq1i.1 |
Ref | Expression |
---|---|
eleq1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1i.1 | . 2 | |
2 | eleq1 2180 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: eleq12i 2185 eqeltri 2190 intexrabim 4048 abssexg 4076 abnex 4338 snnex 4339 pwexb 4365 sucexb 4383 omex 4477 iprc 4777 dfse2 4882 fressnfv 5575 fnotovb 5782 f1stres 6025 f2ndres 6026 ottposg 6120 dftpos4 6128 frecabex 6263 oacl 6324 diffifi 6756 djuexb 6897 pitonn 7624 axicn 7639 pnfnre 7775 mnfnre 7776 0mnnnnn0 8977 nprmi 11732 txdis1cn 12374 xmeterval 12531 expcncf 12688 bj-sucexg 13047 |
Copyright terms: Public domain | W3C validator |