Theorem riotacl 7133

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 4058	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 7132	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sseldi 3967	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2114  ∃!wreu 3142  {crab 3144  ℩crio 7115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-un 3943  df-in 3945  df-ss 3954  df-sn 4570  df-pr 4572  df-uni 4841  df-iota 6316  df-riota 7116

This theorem is referenced by:  riotaeqimp  7142  riotaprop  7143  riotass2  7146  riotass  7147  riotaxfrd  7150  riotaclb  7157  supcl  8924  fisupcl  8935  htalem  9327  dfac8clem  9460  dfac2a  9557  fin23lem22  9751  zorn2lem1  9920  subcl  10887  divcl  11306  lbcl  11594  flcl  13168  cjf  14465  sqrtcl  14723  qnumdencl  16081  qnumdenbi  16086  catidcl  16955  lubcl  17597  glbcl  17610  ismgmid  17877  grpinvfval  18144  grpinvf  18152  pj1f  18825  mirf  26448  midf  26564  ismidb  26566  lmif  26573  islmib  26575  uspgredg2vlem  27007  usgredg2vlem1  27009  frgrncvvdeqlem4  28083  grpoidcl  28293  grpoinvcl  28303  pjpreeq  29177  cnlnadjlem3  29848  adjbdln  29862  xdivcld  30601  cvmlift3lem3  32570  nosupno  33205  nosupbday  33207  nosupbnd1  33216  scutcut  33268  transportcl  33496  finxpreclem4  34677  poimirlem26  34920  iorlid  35138  riotaclbgBAD  36092  lshpkrlem2  36249  lshpkrcl  36254  cdleme25cl  37495  cdleme29cl  37515  cdlemefrs29clN  37537  cdlemk29-3  38049  cdlemkid5  38073  dihlsscpre  38372  mapdhcl  38865  hdmapcl  38968  hgmapcl  39027  rernegcl  39208  rersubcl  39215  wessf1ornlem  41452  fourierdlem50  42448