Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqriv | Unicode version |
Description: Infer equality of classes from equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqriv.1 |
Ref | Expression |
---|---|
eqriv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2111 | . 2 | |
2 | eqriv.1 | . 2 | |
3 | 1, 2 | mpgbir 1414 | 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-gen 1410 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: eqid 2117 sb8ab 2239 cbvab 2240 vjust 2661 nfccdeq 2880 difeqri 3166 uneqri 3188 incom 3238 ineqri 3239 difin 3283 invdif 3288 indif 3289 difundi 3298 indifdir 3302 pwv 3705 uniun 3725 intun 3772 intpr 3773 iuncom 3789 iuncom4 3790 iun0 3839 0iun 3840 iunin2 3846 iunun 3861 iunxun 3862 iunxiun 3864 iinpw 3873 inuni 4050 unidif0 4061 unipw 4109 snnex 4339 unon 4397 xpiundi 4567 xpiundir 4568 0xp 4589 iunxpf 4657 cnvuni 4695 dmiun 4718 dmuni 4719 epini 4880 rniun 4919 cnvresima 4998 imaco 5014 rnco 5015 dfmpt3 5215 imaiun 5629 opabex3d 5987 opabex3 5988 ecid 6460 qsid 6462 mapval2 6540 ixpin 6585 dfz2 9081 infssuzex 11554 1nprm 11707 |
Copyright terms: Public domain | W3C validator |