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 2034 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
2 | eqriv.1 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) | |
3 | 1, 2 | mpgbir 1342 | 1 ⊢ 𝐴 = 𝐵 |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1243 ∈ wcel 1393 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-gen 1338 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: eqid 2040 sb8ab 2159 cbvab 2160 vjust 2558 nfccdeq 2762 difeqri 3064 uneqri 3085 incom 3129 ineqri 3130 difin 3174 invdif 3179 indif 3180 difundi 3189 indifdir 3193 pwv 3579 uniun 3599 intun 3646 intpr 3647 iuncom 3663 iuncom4 3664 iun0 3713 0iun 3714 iunin2 3720 iunun 3734 iunxun 3735 iunxiun 3736 iinpw 3742 inuni 3909 unidif0 3920 unipw 3953 snnex 4181 unon 4237 xpiundi 4398 xpiundir 4399 0xp 4420 iunxpf 4484 cnvuni 4521 dmiun 4544 dmuni 4545 epini 4696 rniun 4734 cnvresima 4810 imaco 4826 rnco 4827 dfmpt3 5021 imaiun 5399 opabex3d 5748 opabex3 5749 ecid 6169 qsid 6171 dfz2 8313 |
Copyright terms: Public domain | W3C validator |