Theorem riotacl 6503

Description: Closure of restricted iota. (Contributed by NM, 21-Aug-2011.)

Assertion

Ref	Expression
riotacl	⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem riotacl

Step	Hyp	Ref	Expression
1		ssrab2 3649	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 6502	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sseldi 3565	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 1976  ∃!wreu 2897  {crab 2899  ℩crio 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-un 3544  df-in 3546  df-ss 3553  df-sn 4125  df-pr 4127  df-uni 4367  df-iota 5754  df-riota 6489

This theorem is referenced by:  riotaprop  6512  riotass2  6515  riotass  6516  riotaxfrd  6519  riotaclb  6526  supcl  8224  fisupcl  8235  htalem  8619  dfac8clem  8715  dfac2a  8812  fin23lem22  9009  zorn2lem1  9178  subcl  10131  divcl  10540  lbcl  10823  flcl  12413  cjf  13638  sqrtcl  13895  qnumdencl  15231  qnumdenbi  15236  catidcl  16112  lubcl  16754  glbcl  16767  ismgmid  17033  grpinvf  17235  pj1f  17879  mirf  25273  midf  25386  ismidb  25388  lmif  25395  islmib  25397  usgraidx2vlem1  25686  nbgraf1olem2  25737  frgrancvvdeqlem5  26327  grpoidcl  26518  grpoinvcl  26528  pjpreeq  27447  cnlnadjlem3  28118  adjbdln  28132  xdivcld  28768  cvmlift3lem3  30363  transportcl  31116  finxpreclem4  32203  poimirlem26  32401  iorlid  32623  riotaclbgBAD  33054  lshpkrlem2  33212  lshpkrcl  33217  cdleme25cl  34459  cdleme29cl  34479  cdlemefrs29clN  34501  cdlemk29-3  35013  cdlemkid5  35037  dihlsscpre  35337  mapdhcl  35830  hdmapcl  35936  hgmapcl  35995  wessf1ornlem  38162  fourierdlem50  38846  riotaeqimp  40158  uspgredg2vlem  40445  usgredg2vlem1  40447  frgrncvvdeqlem5  41468