Theorem riotacl 7131

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

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

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570  df-uni 4839  df-iota 6314  df-riota 7114

This theorem is referenced by:  riotaeqimp  7140  riotaprop  7141  riotass2  7144  riotass  7145  riotaxfrd  7148  riotaclb  7155  supcl  8922  fisupcl  8933  htalem  9325  dfac8clem  9458  dfac2a  9555  fin23lem22  9749  zorn2lem1  9918  subcl  10885  divcl  11304  lbcl  11592  flcl  13166  cjf  14463  sqrtcl  14721  qnumdencl  16079  qnumdenbi  16084  catidcl  16953  lubcl  17595  glbcl  17608  ismgmid  17875  grpinvfval  18142  grpinvf  18150  pj1f  18823  mirf  26446  midf  26562  ismidb  26564  lmif  26571  islmib  26573  uspgredg2vlem  27005  usgredg2vlem1  27007  frgrncvvdeqlem4  28081  grpoidcl  28291  grpoinvcl  28301  pjpreeq  29175  cnlnadjlem3  29846  adjbdln  29860  xdivcld  30599  cvmlift3lem3  32568  nosupno  33203  nosupbday  33205  nosupbnd1  33214  scutcut  33266  transportcl  33494  finxpreclem4  34678  poimirlem26  34933  iorlid  35151  riotaclbgBAD  36105  lshpkrlem2  36262  lshpkrcl  36267  cdleme25cl  37508  cdleme29cl  37528  cdlemefrs29clN  37550  cdlemk29-3  38062  cdlemkid5  38086  dihlsscpre  38385  mapdhcl  38878  hdmapcl  38981  hgmapcl  39040  rernegcl  39221  rersubcl  39228  wessf1ornlem  41465  fourierdlem50  42461