Theorem riotacl2 7331

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 3351	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		iotacl 6478	. . 3 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
3	1, 2	sylbi 217	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
4		df-riota 7315	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rab 3400	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	3, 4, 5	3eltr4g 2853	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃!weu 2568  {cab 2714  ∃!wreu 3348  {crab 3399  ℩cio 6446  ℩crio 7314

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448  df-riota 7315

This theorem is referenced by:  riotacl  7332  riotasbc  7333  riotaxfrd  7349  supub  9362  suplub  9363  ordtypelem3  9425  catlid  17606  catrid  17607  grplinv  18919  pj1id  19628  evlsval2  22042  ig1pval3  26139  coelem  26187  quotlem  26264  mircgr  28729  mirbtwn  28730  grpoidinv2  30590  grpoinv  30600  cnlnadjlem5  32146  cvmsiota  35471  cvmliftiota  35495  weiunlem  36657  weiunfrlem  36658  linvh  42346  mpaalem  43390  disjinfi  45432