New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 | ⊢ (x ∈ A ↔ x ∈ B) |
Ref | Expression |
---|---|
eqriv | ⊢ A = B |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfcleq 2347 | . 2 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B)) | |
2 | eqriv.1 | . 2 ⊢ (x ∈ A ↔ x ∈ B) | |
3 | 1, 2 | mpgbir 1550 | 1 ⊢ A = B |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 = wceq 1642 ∈ wcel 1710 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-cleq 2346 |
This theorem is referenced by: eqid 2353 cbvab 2471 vjust 2860 nincom 3226 dblcompl 3227 difeqri 3387 uneqri 3406 incom 3448 ineqri 3449 indifdir 3511 undif3 3515 complab 3524 pwpr 3883 pwtp 3884 pwv 3886 unipr 3905 uniun 3910 intun 3958 intpr 3959 iuncom 3975 iuncom4 3976 iun0 4022 0iun 4023 iunin2 4030 iinun2 4032 iundif2 4033 iunun 4046 iunxun 4047 iunxiun 4048 iinuni 4049 iinpw 4054 unipw 4117 pwadjoin 4119 pw1un 4163 pw1in 4164 pw1sn 4165 df1c2 4168 imacok 4282 dfuni12 4291 dfimak2 4298 dfpw12 4301 dfuni3 4315 dfint3 4318 unipw1 4325 dfpw2 4327 addcid1 4405 addcass 4415 dfphi2 4569 proj1op 4600 proj2op 4601 setconslem4 4734 dfswap2 4741 xpiundi 4817 xpiundir 4818 iunxpf 4829 xp0r 4842 cnvuni 4895 dfrn4 4904 dmuni 4914 dfima3 4951 rnuni 5038 dmsnopg 5066 rnsnop 5075 cnvresima 5077 imaco 5086 rnco 5087 dfxp2 5113 imaiun 5464 dfdm4 5507 dfrn5 5508 dmsi 5519 dmtxp 5802 clos1baseima 5883 qsid 5990 mapval2 6018 |
Copyright terms: Public domain | W3C validator |