Theorem riotacl 6625

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃!wreu 2914  {crab 2916  ℩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-in 3581  df-ss 3588  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  riotaeqimp  6634  riotaprop  6635  riotass2  6638  riotass  6639  riotaxfrd  6642  riotaclb  6649  supcl  8364  fisupcl  8375  htalem  8759  dfac8clem  8855  dfac2a  8952  fin23lem22  9149  zorn2lem1  9318  subcl  10280  divcl  10691  lbcl  10974  flcl  12596  cjf  13844  sqrtcl  14101  qnumdencl  15447  qnumdenbi  15452  catidcl  16343  lubcl  16985  glbcl  16998  ismgmid  17264  grpinvf  17466  pj1f  18110  mirf  25555  midf  25668  ismidb  25670  lmif  25677  islmib  25679  uspgredg2vlem  26115  usgredg2vlem1  26117  frgrncvvdeqlem4  27166  grpoidcl  27368  grpoinvcl  27378  pjpreeq  28257  cnlnadjlem3  28928  adjbdln  28942  xdivcld  29631  cvmlift3lem3  31303  nosupno  31849  nosupbday  31851  nosupbnd1  31860  scutcut  31912  transportcl  32140  finxpreclem4  33231  poimirlem26  33435  iorlid  33657  riotaclbgBAD  34240  lshpkrlem2  34398  lshpkrcl  34403  cdleme25cl  35645  cdleme29cl  35665  cdlemefrs29clN  35687  cdlemk29-3  36199  cdlemkid5  36223  dihlsscpre  36523  mapdhcl  37016  hdmapcl  37122  hgmapcl  37181  wessf1ornlem  39371  fourierdlem50  40373