Metamath Proof Explorer

Theorem riotasv3d

Description: A property ch holding for a representative of a single-valued class expression C ( y ) (see e.g. reusv2 ) also holds for its description binder D (in the form of property th ). (Contributed by NM, 5-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riotasv3d.1 ⊢ Ⅎ y φ
riotasv3d.2 ⊢ φ → Ⅎ y θ
riotasv3d.3 ⊢ φ → D = ι x ∈ A | ∀ y ∈ B ψ → x = C
riotasv3d.4 ⊢ φ ∧ C = D → χ ↔ θ
riotasv3d.5 ⊢ φ → y ∈ B ∧ ψ → χ
riotasv3d.6 ⊢ φ → D ∈ A
riotasv3d.7 ⊢ φ → ∃ y ∈ B ψ
Assertion riotasv3d ⊢ φ ∧ A ∈ V → θ

Proof

Step Hyp Ref Expression
1 riotasv3d.1 ⊢ Ⅎ y φ
2 riotasv3d.2 ⊢ φ → Ⅎ y θ
3 riotasv3d.3 ⊢ φ → D = ι x ∈ A | ∀ y ∈ B ψ → x = C
4 riotasv3d.4 ⊢ φ ∧ C = D → χ ↔ θ
5 riotasv3d.5 ⊢ φ → y ∈ B ∧ ψ → χ
6 riotasv3d.6 ⊢ φ → D ∈ A
7 riotasv3d.7 ⊢ φ → ∃ y ∈ B ψ
8 elex ⊢ A ∈ V → A ∈ V
9 7 adantr ⊢ φ ∧ A ∈ V → ∃ y ∈ B ψ
10 nfv ⊢ Ⅎ y A ∈ V
11 5 imp ⊢ φ ∧ y ∈ B ∧ ψ → χ
12 11 adantrl ⊢ φ ∧ A ∈ V ∧ y ∈ B ∧ ψ → χ
13 3 6 riotasvd ⊢ φ ∧ A ∈ V → y ∈ B ∧ ψ → D = C
14 13 impr ⊢ φ ∧ A ∈ V ∧ y ∈ B ∧ ψ → D = C
15 14 eqcomd ⊢ φ ∧ A ∈ V ∧ y ∈ B ∧ ψ → C = D
16 15 4 syldan ⊢ φ ∧ A ∈ V ∧ y ∈ B ∧ ψ → χ ↔ θ
17 12 16 mpbid ⊢ φ ∧ A ∈ V ∧ y ∈ B ∧ ψ → θ
18 17 exp45 ⊢ φ → A ∈ V → y ∈ B → ψ → θ
19 1 10 18 ralrimd ⊢ φ → A ∈ V → ∀ y ∈ B ψ → θ
20 r19.23t ⊢ Ⅎ y θ → ∀ y ∈ B ψ → θ ↔ ∃ y ∈ B ψ → θ
21 2 20 syl ⊢ φ → ∀ y ∈ B ψ → θ ↔ ∃ y ∈ B ψ → θ
22 19 21 sylibd ⊢ φ → A ∈ V → ∃ y ∈ B ψ → θ
23 22 imp ⊢ φ ∧ A ∈ V → ∃ y ∈ B ψ → θ
24 9 23 mpd ⊢ φ ∧ A ∈ V → θ
25 8 24 sylan2 ⊢ φ ∧ A ∈ V → θ