# Metamath Proof Explorer

## Theorem fvmptex

Description: Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that (IB ) is just shorthand for if ( B e. V , B , (/) ) , and it is always a set by fvex .) Note also that these functions are not the same; wherever B ( C ) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G , and G ( C ) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fvmptex.1 $⊢ F = x ∈ A ⟼ B$
fvmptex.2 $⊢ G = x ∈ A ⟼ I ⁡ B$
Assertion fvmptex $⊢ F ⁡ C = G ⁡ C$

### Proof

Step Hyp Ref Expression
1 fvmptex.1 $⊢ F = x ∈ A ⟼ B$
2 fvmptex.2 $⊢ G = x ∈ A ⟼ I ⁡ B$
3 csbeq1
4 nfcv $⊢ Ⅎ _ y B$
5 nfcsb1v
6 csbeq1a
7 4 5 6 cbvmpt
8 1 7 eqtri
9 3 8 fvmpti
10 3 fveq2d
11 nfcv $⊢ Ⅎ _ y I ⁡ B$
12 nfcv $⊢ Ⅎ _ x I$
13 12 5 nffv
14 6 fveq2d
15 11 13 14 cbvmpt
16 2 15 eqtri
17 fvex
18 10 16 17 fvmpt
19 9 18 eqtr4d $⊢ C ∈ A → F ⁡ C = G ⁡ C$
20 1 dmmptss $⊢ dom ⁡ F ⊆ A$
21 20 sseli $⊢ C ∈ dom ⁡ F → C ∈ A$
22 ndmfv $⊢ ¬ C ∈ dom ⁡ F → F ⁡ C = ∅$
23 21 22 nsyl5 $⊢ ¬ C ∈ A → F ⁡ C = ∅$
24 fvex $⊢ I ⁡ B ∈ V$
25 24 2 dmmpti $⊢ dom ⁡ G = A$
26 25 eleq2i $⊢ C ∈ dom ⁡ G ↔ C ∈ A$
27 ndmfv $⊢ ¬ C ∈ dom ⁡ G → G ⁡ C = ∅$
28 26 27 sylnbir $⊢ ¬ C ∈ A → G ⁡ C = ∅$
29 23 28 eqtr4d $⊢ ¬ C ∈ A → F ⁡ C = G ⁡ C$
30 19 29 pm2.61i $⊢ F ⁡ C = G ⁡ C$