![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqriv | GIF 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 2183 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1464 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1364 ∈ wcel 2160 |
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 1460 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: eqid 2189 sb8ab 2311 cbvabw 2312 cbvab 2313 vjust 2753 nfccdeq 2975 csbcow 3083 difeqri 3270 uneqri 3292 incom 3342 ineqri 3343 difin 3387 invdif 3392 indif 3393 difundi 3402 indifdir 3406 pwv 3823 uniun 3843 intun 3890 intpr 3891 iuncom 3907 iuncom4 3908 iun0 3958 0iun 3959 iunin2 3965 iunun 3980 iunxun 3981 iunxiun 3983 iinpw 3992 inuni 4173 unidif0 4185 unipw 4235 snnex 4466 unon 4528 xpiundi 4702 xpiundir 4703 0xp 4724 iunxpf 4793 cnvuni 4831 dmiun 4854 dmuni 4855 epini 5017 rniun 5057 cnvresima 5136 imaco 5152 rnco 5153 dfmpt3 5357 imaiun 5782 opabex3d 6146 opabex3 6147 ecid 6624 qsid 6626 mapval2 6704 ixpin 6749 dfz2 9355 dfrp2 10294 infssuzex 11982 1nprm 12146 infpn2 12507 |
Copyright terms: Public domain | W3C validator |