Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > riotacl2 | Structured version Visualization version Unicode version |
Description: Membership law for
"the unique element in such that ."
(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.) |
Ref | Expression |
---|---|
riotacl2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-reu 2919 | . . 3 | |
2 | iotacl 5874 | . . 3 | |
3 | 1, 2 | sylbi 207 | . 2 |
4 | df-riota 6611 | . 2 | |
5 | df-rab 2921 | . 2 | |
6 | 3, 4, 5 | 3eltr4g 2718 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wcel 1990 weu 2470 cab 2608 wreu 2914 crab 2916 cio 5849 crio 6610 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-un 3579 df-sn 4178 df-pr 4180 df-uni 4437 df-iota 5851 df-riota 6611 |
This theorem is referenced by: riotacl 6625 riotasbc 6626 riotaxfrd 6642 supub 8365 suplub 8366 ordtypelem3 8425 catlid 16344 catrid 16345 grplinv 17468 pj1id 18112 evlsval2 19520 ig1pval3 23934 coelem 23982 quotlem 24055 mircgr 25552 mirbtwn 25553 grpoidinv2 27369 grpoinv 27379 cnlnadjlem5 28930 cvmsiota 31259 cvmliftiota 31283 mpaalem 37722 disjinfi 39380 |
Copyright terms: Public domain | W3C validator |