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

Metamath Proof Explorer

Theorem fvmpti

Description: Value of a function given in maps-to notation. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fvmptg.1 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
fvmptg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
Assertion fvmpti ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 fvmptg.1 ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 )
2 fvmptg.2 ⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 )
3 1 2 fvmptg ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 )
4 fvi ⊢ ( 𝐶 ∈ V → ( I ‘ 𝐶 ) = 𝐶 )
5 4 adantl ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( I ‘ 𝐶 ) = 𝐶 )
6 3 5 eqtr4d ⊢ ( ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
7 1 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝐵 ∈ V ↔ 𝐶 ∈ V ) )
8 2 dmmpt ⊢ dom 𝐹 = { 𝑥 ∈ 𝐷 ∣ 𝐵 ∈ V }
9 7 8 elrab2 ⊢ ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐴 ∈ 𝐷 ∧ 𝐶 ∈ V ) )
10 9 baib ⊢ ( 𝐴 ∈ 𝐷 → ( 𝐴 ∈ dom 𝐹 ↔ 𝐶 ∈ V ) )
11 10 notbid ⊢ ( 𝐴 ∈ 𝐷 → ( ¬ 𝐴 ∈ dom 𝐹 ↔ ¬ 𝐶 ∈ V ) )
12 ndmfv ⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
13 11 12 biimtrrdi ⊢ ( 𝐴 ∈ 𝐷 → ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
14 13 imp ⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
15 fvprc ⊢ ( ¬ 𝐶 ∈ V → ( I ‘ 𝐶 ) = ∅ )
16 15 adantl ⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( I ‘ 𝐶 ) = ∅ )
17 14 16 eqtr4d ⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )
18 6 17 pm2.61dan ⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) )