Theorem riotacl2 7393

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 3374	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		iotacl 6534	. . 3 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
3	1, 2	sylbi 216	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) ∈ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)})
4		df-riota 7376	. 2 ⊢ (℩𝑥 ∈ 𝐴 𝜑) = (℩𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-rab 3430	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6	3, 4, 5	3eltr4g 2846	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → (℩𝑥 ∈ 𝐴 𝜑) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  ∃!weu 2558  {cab 2705  ∃!wreu 3371  {crab 3429  ℩cio 6498  ℩crio 7375

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-un 3952  df-in 3954  df-ss 3964  df-sn 4630  df-pr 4632  df-uni 4909  df-iota 6500  df-riota 7376

This theorem is referenced by:  riotacl  7394  riotasbc  7395  riotaxfrd  7411  supub  9483  suplub  9484  ordtypelem3  9544  catlid  17663  catrid  17664  grplinv  18946  pj1id  19654  evlsval2  22033  ig1pval3  26125  coelem  26173  quotlem  26248  mircgr  28474  mirbtwn  28475  grpoidinv2  30338  grpoinv  30348  cnlnadjlem5  31894  cvmsiota  34887  cvmliftiota  34911  linvh  41566  mpaalem  42576  disjinfi  44565

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »