![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > moeq | Structured version Visualization version Unicode version |
Description: There is at most one set equal to a class. (Contributed by NM, 8-Mar-1995.) |
Ref | Expression |
---|---|
moeq |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isset 3061 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eueq 3222 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitr3i 259 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | biimpi 199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-mo 2315 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | mpbir 214 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-v 3059 |
This theorem is referenced by: mosub 3228 euxfr2 3235 reueq 3248 rmoeq 3249 sndisj 4410 disjxsn 4412 reusv1 4620 reusv2lem1 4621 reuxfr2d 4640 funopabeq 5639 funcnvsn 5650 fvmptg 5974 fvopab6 6003 ovmpt4g 6451 ov3 6465 ov6g 6466 oprabex3 6814 1stconst 6916 2ndconst 6917 iunmapdisj 8485 axaddf 9600 axmulf 9601 joinfval 16302 joinval 16306 meetfval 16316 meetval 16320 reuxfr3d 28181 abrexdom2jm 28198 abrexdom2 32104 |
Copyright terms: Public domain | W3C validator |