Metamath Proof Explorer

Theorem fvunsn

Description: Remove an ordered pair not participating in a function value. (Contributed by NM, 1-Oct-2013) (Revised by Mario Carneiro, 28-May-2014)

Ref Expression
Assertion fvunsn ( 𝐵 ≠ 𝐷 → ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 ) = ( 𝐴 ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 resundir ⊢ ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) = ( ( 𝐴 ↾ { 𝐷 } ) ∪ ( { ⟨ 𝐵 , 𝐶 ⟩ } ↾ { 𝐷 } ) )
2 nelsn ⊢ ( 𝐵 ≠ 𝐷 → ¬ 𝐵 ∈ { 𝐷 } )
3 ressnop0 ⊢ ( ¬ 𝐵 ∈ { 𝐷 } → ( { ⟨ 𝐵 , 𝐶 ⟩ } ↾ { 𝐷 } ) = ∅ )
4 2 3 syl ⊢ ( 𝐵 ≠ 𝐷 → ( { ⟨ 𝐵 , 𝐶 ⟩ } ↾ { 𝐷 } ) = ∅ )
5 4 uneq2d ⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 ↾ { 𝐷 } ) ∪ ( { ⟨ 𝐵 , 𝐶 ⟩ } ↾ { 𝐷 } ) ) = ( ( 𝐴 ↾ { 𝐷 } ) ∪ ∅ ) )
6 un0 ⊢ ( ( 𝐴 ↾ { 𝐷 } ) ∪ ∅ ) = ( 𝐴 ↾ { 𝐷 } )
7 5 6 eqtrdi ⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 ↾ { 𝐷 } ) ∪ ( { ⟨ 𝐵 , 𝐶 ⟩ } ↾ { 𝐷 } ) ) = ( 𝐴 ↾ { 𝐷 } ) )
8 1 7 eqtrid ⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) = ( 𝐴 ↾ { 𝐷 } ) )
9 8 fveq1d ⊢ ( 𝐵 ≠ 𝐷 → ( ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) ‘ 𝐷 ) = ( ( 𝐴 ↾ { 𝐷 } ) ‘ 𝐷 ) )
10 fvressn ⊢ ( 𝐷 ∈ V → ( ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) ‘ 𝐷 ) = ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 ) )
11 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) ‘ 𝐷 ) = ∅ )
12 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 ) = ∅ )
13 11 12 eqtr4d ⊢ ( ¬ 𝐷 ∈ V → ( ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) ‘ 𝐷 ) = ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 ) )
14 10 13 pm2.61i ⊢ ( ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ↾ { 𝐷 } ) ‘ 𝐷 ) = ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 )
15 fvressn ⊢ ( 𝐷 ∈ V → ( ( 𝐴 ↾ { 𝐷 } ) ‘ 𝐷 ) = ( 𝐴 ‘ 𝐷 ) )
16 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( ( 𝐴 ↾ { 𝐷 } ) ‘ 𝐷 ) = ∅ )
17 fvprc ⊢ ( ¬ 𝐷 ∈ V → ( 𝐴 ‘ 𝐷 ) = ∅ )
18 16 17 eqtr4d ⊢ ( ¬ 𝐷 ∈ V → ( ( 𝐴 ↾ { 𝐷 } ) ‘ 𝐷 ) = ( 𝐴 ‘ 𝐷 ) )
19 15 18 pm2.61i ⊢ ( ( 𝐴 ↾ { 𝐷 } ) ‘ 𝐷 ) = ( 𝐴 ‘ 𝐷 )
20 9 14 19 3eqtr3g ⊢ ( 𝐵 ≠ 𝐷 → ( ( 𝐴 ∪ { ⟨ 𝐵 , 𝐶 ⟩ } ) ‘ 𝐷 ) = ( 𝐴 ‘ 𝐷 ) )