![]() |
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 2089 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1394 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1296 ∈ wcel 1445 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1390 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-cleq 2088 |
This theorem is referenced by: eqid 2095 sb8ab 2216 cbvab 2217 vjust 2634 nfccdeq 2852 difeqri 3135 uneqri 3157 incom 3207 ineqri 3208 difin 3252 invdif 3257 indif 3258 difundi 3267 indifdir 3271 pwv 3674 uniun 3694 intun 3741 intpr 3742 iuncom 3758 iuncom4 3759 iun0 3808 0iun 3809 iunin2 3815 iunun 3830 iunxun 3831 iunxiun 3832 iinpw 3841 inuni 4012 unidif0 4023 unipw 4068 snnex 4298 unon 4356 xpiundi 4525 xpiundir 4526 0xp 4547 iunxpf 4615 cnvuni 4653 dmiun 4676 dmuni 4677 epini 4836 rniun 4875 cnvresima 4954 imaco 4970 rnco 4971 dfmpt3 5170 imaiun 5577 opabex3d 5930 opabex3 5931 ecid 6395 qsid 6397 mapval2 6475 ixpin 6520 dfz2 8917 infssuzex 11372 1nprm 11523 |
Copyright terms: Public domain | W3C validator |