Theorem riotacl2 7396

Description: Membership law for "the unique element in 𝐴 such that 𝜑". (Contributed by NM, 21-Aug-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Assertion

Ref	Expression
riotacl2	⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})

Proof of Theorem riotacl2

Step	Hyp	Ref	Expression
1		df-reu 3373	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		iotacl 6529	. . 3 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
3	1, 2	sylbi 220	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
4		df-riota 7380	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rab 3420	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	3, 4, 5	3eltr4g 2883	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃!weu 2599  {cab 2744  ∃!wreu 3370  {crab 3419  ℩cio 6497  ℩crio 7379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597  df-uni 4878  df-iota 6499  df-riota 7380

This theorem is used by:  riotacl  7397  riotasbc  7398  riotaxfrd  7414  supub  9429  suplub  9430  ordtypelem3  9492  catlid  17764  catrid  17765  grplinv  19087  pj1id  19800  evlsval2  22275  ig1pval3  26372  coelem  26420  quotlem  26498  mircgr  28971  mirbtwn  28972  grpoidinv2  30904  grpoinv  30914  cnlnadjlem5  32460  cvmsiota  35790  cvmliftiota  35814  weiunlem  37015  weiunfrlem  37016  linvh  42904  mpaalem  43920  disjinfi  45951