Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > dfcleq | Unicode version |
Description: The same as df-cleq 2110 with the hypothesis removed using the Axiom of Extensionality ax-ext 2099. (Contributed by NM, 15-Sep-1993.) |
Ref | Expression |
---|---|
dfcleq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2099 | . 2 | |
2 | 1 | df-cleq 2110 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wal 1314 wceq 1316 wcel 1465 |
This theorem was proved from axioms: ax-ext 2099 |
This theorem depends on definitions: df-cleq 2110 |
This theorem is referenced by: cvjust 2112 eqriv 2114 eqrdv 2115 eqcom 2119 eqeq1 2124 eleq2 2181 cleqh 2217 abbi 2231 nfeq 2266 nfeqd 2273 cleqf 2282 eqss 3082 ddifstab 3178 ssequn1 3216 eqv 3352 disj3 3385 undif4 3395 vnex 4029 inex1 4032 zfpair2 4102 sucel 4302 uniex2 4328 bj-vprc 13021 bdinex1 13024 bj-zfpair2 13035 bj-uniex2 13041 |
Copyright terms: Public domain | W3C validator |