Metamath Proof Explorer


Theorem riotasvd

Description: Deduction version of riotasv . (Contributed by NM, 4-Mar-2013) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses riotasvd.1 ( 𝜑𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) )
riotasvd.2 ( 𝜑𝐷𝐴 )
Assertion riotasvd ( ( 𝜑𝐴𝑉 ) → ( ( 𝑦𝐵𝜓 ) → 𝐷 = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 riotasvd.1 ( 𝜑𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) )
2 riotasvd.2 ( 𝜑𝐷𝐴 )
3 1 adantr ( ( 𝜑𝐴𝑉 ) → 𝐷 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) )
4 2 adantr ( ( 𝜑𝐴𝑉 ) → 𝐷𝐴 )
5 3 4 eqeltrrd ( ( 𝜑𝐴𝑉 ) → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) ∈ 𝐴 )
6 riotaclbgBAD ( 𝐴𝑉 → ( ∃! 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ↔ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) ∈ 𝐴 ) )
7 6 adantl ( ( 𝜑𝐴𝑉 ) → ( ∃! 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ↔ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) ∈ 𝐴 ) )
8 5 7 mpbird ( ( 𝜑𝐴𝑉 ) → ∃! 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) )
9 riotasbc ( ∃! 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) → [ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) / 𝑥 ]𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) )
10 8 9 syl ( ( 𝜑𝐴𝑉 ) → [ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) / 𝑥 ]𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) )
11 eqeq1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝐶𝑧 = 𝐶 ) )
12 11 imbi2d ( 𝑥 = 𝑧 → ( ( 𝜓𝑥 = 𝐶 ) ↔ ( 𝜓𝑧 = 𝐶 ) ) )
13 12 ralbidv ( 𝑥 = 𝑧 → ( ∀ 𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ↔ ∀ 𝑦𝐵 ( 𝜓𝑧 = 𝐶 ) ) )
14 nfra1 𝑦𝑦𝐵 ( 𝜓𝑥 = 𝐶 )
15 nfcv 𝑦 𝐴
16 14 15 nfriota 𝑦 ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) )
17 16 nfeq2 𝑦 𝑧 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) )
18 eqeq1 ( 𝑧 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) → ( 𝑧 = 𝐶 ↔ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) )
19 18 imbi2d ( 𝑧 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) → ( ( 𝜓𝑧 = 𝐶 ) ↔ ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
20 17 19 ralbid ( 𝑧 = ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) → ( ∀ 𝑦𝐵 ( 𝜓𝑧 = 𝐶 ) ↔ ∀ 𝑦𝐵 ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
21 13 20 sbcie2g ( ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) ∈ 𝐴 → ( [ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) / 𝑥 ]𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ↔ ∀ 𝑦𝐵 ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
22 5 21 syl ( ( 𝜑𝐴𝑉 ) → ( [ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) / 𝑥 ]𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ↔ ∀ 𝑦𝐵 ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
23 10 22 mpbid ( ( 𝜑𝐴𝑉 ) → ∀ 𝑦𝐵 ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) )
24 rsp ( ∀ 𝑦𝐵 ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) → ( 𝑦𝐵 → ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
25 23 24 syl ( ( 𝜑𝐴𝑉 ) → ( 𝑦𝐵 → ( 𝜓 → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) ) )
26 25 impd ( ( 𝜑𝐴𝑉 ) → ( ( 𝑦𝐵𝜓 ) → ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) )
27 3 eqeq1d ( ( 𝜑𝐴𝑉 ) → ( 𝐷 = 𝐶 ↔ ( 𝑥𝐴𝑦𝐵 ( 𝜓𝑥 = 𝐶 ) ) = 𝐶 ) )
28 26 27 sylibrd ( ( 𝜑𝐴𝑉 ) → ( ( 𝑦𝐵𝜓 ) → 𝐷 = 𝐶 ) )