Metamath Proof Explorer

Theorem riotass2

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 21-Aug-2011) (Revised by NM, 22-Mar-2013)

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

Proof

Step Hyp Ref Expression
1 reuss2 ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ∃! x ∈ A φ
2 simplr ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ∀ x ∈ A φ → ψ
3 riotasbc ⊢ ∃! x ∈ A φ → [˙ ι x ∈ A | φ / x]˙ φ
4 riotacl ⊢ ∃! x ∈ A φ → ι x ∈ A | φ ∈ A
5 rspsbc ⊢ ι x ∈ A | φ ∈ A → ∀ x ∈ A φ → ψ → [˙ ι x ∈ A | φ / x]˙ φ → ψ
6 sbcimg ⊢ ι x ∈ A | φ ∈ A → [˙ ι x ∈ A | φ / x]˙ φ → ψ ↔ [˙ ι x ∈ A | φ / x]˙ φ → [˙ ι x ∈ A | φ / x]˙ ψ
7 5 6 sylibd ⊢ ι x ∈ A | φ ∈ A → ∀ x ∈ A φ → ψ → [˙ ι x ∈ A | φ / x]˙ φ → [˙ ι x ∈ A | φ / x]˙ ψ
8 4 7 syl ⊢ ∃! x ∈ A φ → ∀ x ∈ A φ → ψ → [˙ ι x ∈ A | φ / x]˙ φ → [˙ ι x ∈ A | φ / x]˙ ψ
9 3 8 mpid ⊢ ∃! x ∈ A φ → ∀ x ∈ A φ → ψ → [˙ ι x ∈ A | φ / x]˙ ψ
10 1 2 9 sylc ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → [˙ ι x ∈ A | φ / x]˙ ψ
11 1 4 syl ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ι x ∈ A | φ ∈ A
12 ssel ⊢ A ⊆ B → ι x ∈ A | φ ∈ A → ι x ∈ A | φ ∈ B
13 12 ad2antrr ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ι x ∈ A | φ ∈ A → ι x ∈ A | φ ∈ B
14 11 13 mpd ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ι x ∈ A | φ ∈ B
15 simprr ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ∃! x ∈ B ψ
16 nfriota1 ⊢ Ⅎ _ x ι x ∈ A | φ
17 16 nfsbc1 ⊢ Ⅎ x [˙ ι x ∈ A | φ / x]˙ ψ
18 sbceq1a ⊢ x = ι x ∈ A | φ → ψ ↔ [˙ ι x ∈ A | φ / x]˙ ψ
19 16 17 18 riota2f ⊢ ι x ∈ A | φ ∈ B ∧ ∃! x ∈ B ψ → [˙ ι x ∈ A | φ / x]˙ ψ ↔ ι x ∈ B | ψ = ι x ∈ A | φ
20 14 15 19 syl2anc ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → [˙ ι x ∈ A | φ / x]˙ ψ ↔ ι x ∈ B | ψ = ι x ∈ A | φ
21 10 20 mpbid ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ι x ∈ B | ψ = ι x ∈ A | φ
22 21 eqcomd ⊢ A ⊆ B ∧ ∀ x ∈ A φ → ψ ∧ ∃ x ∈ A φ ∧ ∃! x ∈ B ψ → ι x ∈ A | φ = ι x ∈ B | ψ