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 ⊢ℲyA∈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→θ