Theorem fmptdf2

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	fmptdf2.p	⊢ Ⅎ 𝑥 𝜑
	fmptdf2.a	⊢ Ⅎ 𝑥 𝐴
	fmptdf2.c	⊢ Ⅎ 𝑥 𝐶
	fmptdf2.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
	fmptdf2.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fmptdf2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fmptdf2.p	⊢ Ⅎ 𝑥 𝜑
2		fmptdf2.a	⊢ Ⅎ 𝑥 𝐴
3		fmptdf2.c	⊢ Ⅎ 𝑥 𝐶
4		fmptdf2.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
5		fmptdf2.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	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )