This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem riotasv2d

Description: Value of description binder D for a single-valued class expression C ( y ) (as in e.g. reusv2 ). Special case of riota2f . (Contributed by NM, 2-Mar-2013)

Ref Expression
Hypotheses riotasv2d.1 ⊢ Ⅎ y φ
riotasv2d.2 ⊢ φ → Ⅎ _ y F
riotasv2d.3 ⊢ φ → Ⅎ y χ
riotasv2d.4 ⊢ φ → D = ι x ∈ A | ∀ y ∈ B ψ → x = C
riotasv2d.5 ⊢ φ ∧ y = E → ψ ↔ χ
riotasv2d.6 ⊢ φ ∧ y = E → C = F
riotasv2d.7 ⊢ φ → D ∈ A
riotasv2d.8 ⊢ φ → E ∈ B
riotasv2d.9 ⊢ φ → χ
Assertion riotasv2d ⊢ φ ∧ A ∈ V → D = F

Proof

Step Hyp Ref Expression
1 riotasv2d.1 ⊢ Ⅎ y φ
2 riotasv2d.2 ⊢ φ → Ⅎ _ y F
3 riotasv2d.3 ⊢ φ → Ⅎ y χ
4 riotasv2d.4 ⊢ φ → D = ι x ∈ A | ∀ y ∈ B ψ → x = C
5 riotasv2d.5 ⊢ φ ∧ y = E → ψ ↔ χ
6 riotasv2d.6 ⊢ φ ∧ y = E → C = F
7 riotasv2d.7 ⊢ φ → D ∈ A
8 riotasv2d.8 ⊢ φ → E ∈ B
9 riotasv2d.9 ⊢ φ → χ
10 elex ⊢ A ∈ V → A ∈ V
11 8 adantr ⊢ φ ∧ A ∈ V → E ∈ B
12 9 adantr ⊢ φ ∧ A ∈ V → χ
13 eleq1 ⊢ y = E → y ∈ B ↔ E ∈ B
14 13 adantl ⊢ φ ∧ y = E → y ∈ B ↔ E ∈ B
15 14 5 anbi12d ⊢ φ ∧ y = E → y ∈ B ∧ ψ ↔ E ∈ B ∧ χ
16 6 eqeq2d ⊢ φ ∧ y = E → D = C ↔ D = F
17 15 16 imbi12d ⊢ φ ∧ y = E → y ∈ B ∧ ψ → D = C ↔ E ∈ B ∧ χ → D = F
18 17 adantlr ⊢ φ ∧ A ∈ V ∧ y = E → y ∈ B ∧ ψ → D = C ↔ E ∈ B ∧ χ → D = F
19 4 7 riotasvd ⊢ φ ∧ A ∈ V → y ∈ B ∧ ψ → D = C
20 nfv ⊢ Ⅎ y A ∈ V
21 1 20 nfan ⊢ Ⅎ y φ ∧ A ∈ V
22 nfcvd ⊢ φ ∧ A ∈ V → Ⅎ _ y E
23 nfvd ⊢ φ → Ⅎ y E ∈ B
24 23 3 nfand ⊢ φ → Ⅎ y E ∈ B ∧ χ
25 nfra1 ⊢ Ⅎ y ∀ y ∈ B ψ → x = C
26 nfcv ⊢ Ⅎ _ y A
27 25 26 nfriota ⊢ Ⅎ _ y ι x ∈ A | ∀ y ∈ B ψ → x = C
28 1 4 nfceqdf ⊢ φ → Ⅎ _ y D ↔ Ⅎ _ y ι x ∈ A | ∀ y ∈ B ψ → x = C
29 27 28 mpbiri ⊢ φ → Ⅎ _ y D
30 29 2 nfeqd ⊢ φ → Ⅎ y D = F
31 24 30 nfimd ⊢ φ → Ⅎ y E ∈ B ∧ χ → D = F
32 31 adantr ⊢ φ ∧ A ∈ V → Ⅎ y E ∈ B ∧ χ → D = F
33 11 18 19 21 22 32 vtocldf ⊢ φ ∧ A ∈ V → E ∈ B ∧ χ → D = F
34 11 12 33 mp2and ⊢ φ ∧ A ∈ V → D = F
35 10 34 sylan2 ⊢ φ ∧ A ∈ V → D = F