Metamath Proof Explorer

Theorem riotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Oct-2005) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion riotass ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ A | φ = ι x ∈ B | φ

Proof

Step Hyp Ref Expression
1 reuss ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ∃! x ∈ A φ
2 riotasbc ⊢ ∃! x ∈ A φ → [˙ ι x ∈ A | φ / x]˙ φ
3 1 2 syl ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → [˙ ι x ∈ A | φ / x]˙ φ
4 simp1 ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → A ⊆ B
5 riotacl ⊢ ∃! x ∈ A φ → ι x ∈ A | φ ∈ A
6 1 5 syl ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ A | φ ∈ A
7 4 6 sseldd ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ A | φ ∈ B
8 simp3 ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ∃! x ∈ B φ
9 nfriota1 ⊢ Ⅎ _ x ι x ∈ A | φ
10 9 nfsbc1 ⊢ Ⅎ x [˙ ι x ∈ A | φ / x]˙ φ
11 sbceq1a ⊢ x = ι x ∈ A | φ → φ ↔ [˙ ι x ∈ A | φ / x]˙ φ
12 9 10 11 riota2f ⊢ ι x ∈ A | φ ∈ B ∧ ∃! x ∈ B φ → [˙ ι x ∈ A | φ / x]˙ φ ↔ ι x ∈ B | φ = ι x ∈ A | φ
13 7 8 12 syl2anc ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → [˙ ι x ∈ A | φ / x]˙ φ ↔ ι x ∈ B | φ = ι x ∈ A | φ
14 3 13 mpbid ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ B | φ = ι x ∈ A | φ
15 14 eqcomd ⊢ A ⊆ B ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B φ → ι x ∈ A | φ = ι x ∈ B | φ