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 ⊢ Ⅎ 𝑦 𝜑
riotasv2d.2 ⊢ ( 𝜑 → Ⅎ 𝑦 𝐹 )
riotasv2d.3 ⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
riotasv2d.4 ⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
riotasv2d.5 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( 𝜓 ↔ 𝜒 ) )
riotasv2d.6 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → 𝐶 = 𝐹 )
riotasv2d.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
riotasv2d.8 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
riotasv2d.9 ⊢ ( 𝜑 → 𝜒 )
Assertion riotasv2d ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝐷 = 𝐹 )

Proof

Step Hyp Ref Expression
1 riotasv2d.1 ⊢ Ⅎ 𝑦 𝜑
2 riotasv2d.2 ⊢ ( 𝜑 → Ⅎ 𝑦 𝐹 )
3 riotasv2d.3 ⊢ ( 𝜑 → Ⅎ 𝑦 𝜒 )
4 riotasv2d.4 ⊢ ( 𝜑 → 𝐷 = ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) )
5 riotasv2d.5 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( 𝜓 ↔ 𝜒 ) )
6 riotasv2d.6 ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → 𝐶 = 𝐹 )
7 riotasv2d.7 ⊢ ( 𝜑 → 𝐷 ∈ 𝐴 )
8 riotasv2d.8 ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
9 riotasv2d.9 ⊢ ( 𝜑 → 𝜒 )
10 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
11 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → 𝐸 ∈ 𝐵 )
12 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → 𝜒 )
13 eleq1 ⊢ ( 𝑦 = 𝐸 → ( 𝑦 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵 ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( 𝑦 ∈ 𝐵 ↔ 𝐸 ∈ 𝐵 ) )
15 14 5 anbi12d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) ↔ ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) ) )
16 6 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( 𝐷 = 𝐶 ↔ 𝐷 = 𝐹 ) )
17 15 16 imbi12d ⊢ ( ( 𝜑 ∧ 𝑦 = 𝐸 ) → ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) ↔ ( ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) → 𝐷 = 𝐹 ) ) )
18 17 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ V ) ∧ 𝑦 = 𝐸 ) → ( ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) ↔ ( ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) → 𝐷 = 𝐹 ) ) )
19 4 7 riotasvd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝜓 ) → 𝐷 = 𝐶 ) )
20 nfv ⊢ Ⅎ 𝑦 𝐴 ∈ V
21 1 20 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝐴 ∈ V )
22 nfcvd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → Ⅎ 𝑦 𝐸 )
23 nfvd ⊢ ( 𝜑 → Ⅎ 𝑦 𝐸 ∈ 𝐵 )
24 23 3 nfand ⊢ ( 𝜑 → Ⅎ 𝑦 ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) )
25 nfra1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 )
26 nfcv ⊢ Ⅎ 𝑦 𝐴
27 25 26 nfriota ⊢ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) )
28 1 4 nfceqdf ⊢ ( 𝜑 → ( Ⅎ 𝑦 𝐷 ↔ Ⅎ 𝑦 ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( 𝜓 → 𝑥 = 𝐶 ) ) ) )
29 27 28 mpbiri ⊢ ( 𝜑 → Ⅎ 𝑦 𝐷 )
30 29 2 nfeqd ⊢ ( 𝜑 → Ⅎ 𝑦 𝐷 = 𝐹 )
31 24 30 nfimd ⊢ ( 𝜑 → Ⅎ 𝑦 ( ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) → 𝐷 = 𝐹 ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → Ⅎ 𝑦 ( ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) → 𝐷 = 𝐹 ) )
33 11 18 19 21 22 32 vtocldf ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → ( ( 𝐸 ∈ 𝐵 ∧ 𝜒 ) → 𝐷 = 𝐹 ) )
34 11 12 33 mp2and ⊢ ( ( 𝜑 ∧ 𝐴 ∈ V ) → 𝐷 = 𝐹 )
35 10 34 sylan2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑉 ) → 𝐷 = 𝐹 )