Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elequ2 | Unicode version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elequ2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-14 1492 | . 2 | |
2 | ax-14 1492 | . . 3 | |
3 | 2 | equcoms 1684 | . 2 |
4 | 1, 3 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
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-gen 1425 ax-ie2 1470 ax-8 1482 ax-14 1492 ax-17 1506 ax-i9 1510 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: elsb4 1952 dveel2 1996 axext3 2122 axext4 2123 bm1.1 2124 eleq2w 2201 bm1.3ii 4049 nalset 4058 zfun 4356 fv3 5444 tfrlemisucaccv 6222 tfr1onlemsucaccv 6238 tfrcllemsucaccv 6251 acfun 7063 ccfunen 7079 bdsepnft 13085 bdsepnfALT 13087 bdbm1.3ii 13089 bj-nalset 13093 bj-nnelirr 13151 strcollnft 13182 strcollnfALT 13184 nninfalllem1 13203 nninfsellemeq 13210 nninfsellemqall 13211 nninfsellemeqinf 13212 nninfomni 13215 |
Copyright terms: Public domain | W3C validator |