![]() |
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 2171 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqriv.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbir 1453 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1449 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: eqid 2177 sb8ab 2299 cbvabw 2300 cbvab 2301 vjust 2738 nfccdeq 2960 csbcow 3068 difeqri 3255 uneqri 3277 incom 3327 ineqri 3328 difin 3372 invdif 3377 indif 3378 difundi 3387 indifdir 3391 pwv 3808 uniun 3828 intun 3875 intpr 3876 iuncom 3892 iuncom4 3893 iun0 3943 0iun 3944 iunin2 3950 iunun 3965 iunxun 3966 iunxiun 3968 iinpw 3977 inuni 4155 unidif0 4167 unipw 4217 snnex 4448 unon 4510 xpiundi 4684 xpiundir 4685 0xp 4706 iunxpf 4775 cnvuni 4813 dmiun 4836 dmuni 4837 epini 4999 rniun 5039 cnvresima 5118 imaco 5134 rnco 5135 dfmpt3 5338 imaiun 5760 opabex3d 6121 opabex3 6122 ecid 6597 qsid 6599 mapval2 6677 ixpin 6722 dfz2 9324 dfrp2 10263 infssuzex 11949 1nprm 12113 infpn2 12456 |
Copyright terms: Public domain | W3C validator |