Theorem riotacl 5969

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 3309	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ⊆ 𝐴
2		riotacl2 5968	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})
3	1, 2	sselid 3222	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2200  ∃!wreu 2510  {crab 2512  ℩crio 5952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-uni 3888  df-iota 5277  df-riota 5953

This theorem is referenced by:  riotaeqimp  5978  riotaprop  5979  riotass2  5982  riotass  5983  acexmidlemcase  5995  supclti  7161  caucvgsrlemcl  7972  caucvgsrlemgt1  7978  axcaucvglemcl  8078  subval  8334  subcl  8341  divvalap  8817  divclap  8821  lbcl  9089  divfnzn  9812  flqcl  10488  flapcl  10490  cjval  11351  cjth  11352  cjf  11353  oddpwdclemodd  12689  oddpwdclemdc  12690  oddpwdc  12691  qnumdencl  12704  qnumdenbi  12709  ismgmid  13405  grpinvf  13575  uspgredg2vlem  16012  usgredg2vlem1  16014