Theorem riotacl2 6271

Description: Membership law for "the unique element in such that ."

(Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Assertion

Ref	Expression
riotacl2

Proof of Theorem riotacl2

Step	Hyp	Ref	Expression
1		df-reu 2814	. . 3
2		iotacl 5579	. . 3
3	1, 2	sylbi 195	. 2
4		df-riota 6257	. 2
5		df-rab 2816	. 2
6	3, 4, 5	3eltr4g 2563	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  E!weu 2282  {cab 2442  E!wreu 2809  {crab 2811  iotacio 5554  iota_crio 6256

This theorem is referenced by:  riotacl  6272  riotasbc  6273  riotaxfrd  6288  supub  7939  suplub  7940  ordtypelem3  7966  catlid  15080  catrid  15081  grplinv  16096  pj1id  16717  evlsval2  18189  ig1pval3  22575  coelem  22623  quotlem  22696  mircgr  24038  mirbtwn  24039  grpoidinv2  25220  grpoinv  25229  cnlnadjlem5  26990  cvmsiota  28722  cvmliftiota  28746  mpaalem  31101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250  df-iota 5556  df-riota 6257