Metamath Proof Explorer


Theorem fmptdF

Description: Domain and codomain of the mapping operation; deduction form. This version of fmptd uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017)

Ref Expression
Hypotheses fmptdF.p 𝑥 𝜑
fmptdF.a 𝑥 𝐴
fmptdF.c 𝑥 𝐶
fmptdF.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
fmptdF.2 𝐹 = ( 𝑥𝐴𝐵 )
Assertion fmptdF ( 𝜑𝐹 : 𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 fmptdF.p 𝑥 𝜑
2 fmptdF.a 𝑥 𝐴
3 fmptdF.c 𝑥 𝐶
4 fmptdF.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝐶 )
5 fmptdF.2 𝐹 = ( 𝑥𝐴𝐵 )
6 4 sbimi ( [ 𝑦 / 𝑥 ] ( 𝜑𝑥𝐴 ) → [ 𝑦 / 𝑥 ] 𝐵𝐶 )
7 sban ( [ 𝑦 / 𝑥 ] ( 𝜑𝑥𝐴 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝑥𝐴 ) )
8 1 sbf ( [ 𝑦 / 𝑥 ] 𝜑𝜑 )
9 2 clelsb1fw ( [ 𝑦 / 𝑥 ] 𝑥𝐴𝑦𝐴 )
10 8 9 anbi12i ( ( [ 𝑦 / 𝑥 ] 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝑥𝐴 ) ↔ ( 𝜑𝑦𝐴 ) )
11 7 10 bitri ( [ 𝑦 / 𝑥 ] ( 𝜑𝑥𝐴 ) ↔ ( 𝜑𝑦𝐴 ) )
12 sbsbc ( [ 𝑦 / 𝑥 ] 𝐵𝐶[ 𝑦 / 𝑥 ] 𝐵𝐶 )
13 sbcel12 ( [ 𝑦 / 𝑥 ] 𝐵𝐶 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 )
14 vex 𝑦 ∈ V
15 14 3 csbgfi 𝑦 / 𝑥 𝐶 = 𝐶
16 15 eleq2i ( 𝑦 / 𝑥 𝐵 𝑦 / 𝑥 𝐶 𝑦 / 𝑥 𝐵𝐶 )
17 13 16 bitri ( [ 𝑦 / 𝑥 ] 𝐵𝐶 𝑦 / 𝑥 𝐵𝐶 )
18 12 17 bitri ( [ 𝑦 / 𝑥 ] 𝐵𝐶 𝑦 / 𝑥 𝐵𝐶 )
19 6 11 18 3imtr3i ( ( 𝜑𝑦𝐴 ) → 𝑦 / 𝑥 𝐵𝐶 )
20 19 ralrimiva ( 𝜑 → ∀ 𝑦𝐴 𝑦 / 𝑥 𝐵𝐶 )
21 nfcv 𝑦 𝐴
22 nfcv 𝑦 𝐵
23 nfcsb1v 𝑥 𝑦 / 𝑥 𝐵
24 csbeq1a ( 𝑥 = 𝑦𝐵 = 𝑦 / 𝑥 𝐵 )
25 2 21 22 23 24 cbvmptf ( 𝑥𝐴𝐵 ) = ( 𝑦𝐴 𝑦 / 𝑥 𝐵 )
26 25 fmpt ( ∀ 𝑦𝐴 𝑦 / 𝑥 𝐵𝐶 ↔ ( 𝑥𝐴𝐵 ) : 𝐴𝐶 )
27 20 26 sylib ( 𝜑 → ( 𝑥𝐴𝐵 ) : 𝐴𝐶 )
28 5 feq1i ( 𝐹 : 𝐴𝐶 ↔ ( 𝑥𝐴𝐵 ) : 𝐴𝐶 )
29 27 28 sylibr ( 𝜑𝐹 : 𝐴𝐶 )