![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isseti | Structured version Visualization version Unicode version |
Description: A way to say "![]() |
Ref | Expression |
---|---|
isseti.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
isseti |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isseti.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | isset 3060 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 213 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-12 1943 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-v 3058 |
This theorem is referenced by: rexcom4b 3080 ceqsex 3094 vtoclf 3110 vtocl 3111 vtocl2 3113 vtocl3 3114 vtoclef 3133 eqvinc 3177 euind 3236 eusv2nf 4614 zfpair 4650 axpr 4651 opabn0 4745 isarep2 5684 dfoprab2 6363 rnoprab 6405 ov3 6459 omeu 7311 cflem 8701 genpass 9459 supaddc 10601 supadd 10602 supmul1 10603 supmullem2 10605 supmul 10606 ruclem13 14342 joindm 16297 meetdm 16311 bnj986 29813 bj-snsetex 31601 ac6s6f 32460 elintima 36289 funressnfv 38666 |
Copyright terms: Public domain | W3C validator |