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

Metamath Proof Explorer

Theorem fmptff

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025)

Ref Expression
Hypotheses fmptff.1 
|- F/_ x A
fmptff.2 
|- F/_ x B
fmptff.3 
|- F = ( x e. A |-> C )
Assertion fmptff 
|- ( A. x e. A C e. B <-> F : A --> B )

Proof

Step Hyp Ref Expression
1 fmptff.1 
 |-  F/_ x A
2 fmptff.2 
 |-  F/_ x B
3 fmptff.3 
 |-  F = ( x e. A |-> C )
4 nfcv 
 |-  F/_ y A
5 nfv 
 |-  F/ y C e. B
6 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
7 6 2 nfel 
 |-  F/ x [_ y / x ]_ C e. B
8 csbeq1a 
 |-  ( x = y -> C = [_ y / x ]_ C )
9 8 eleq1d 
 |-  ( x = y -> ( C e. B <-> [_ y / x ]_ C e. B ) )
10 1 4 5 7 9 cbvralfw 
 |-  ( A. x e. A C e. B <-> A. y e. A [_ y / x ]_ C e. B )
11 nfcv 
 |-  F/_ y C
12 1 4 11 6 8 cbvmptf 
 |-  ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
13 3 12 eqtri 
 |-  F = ( y e. A |-> [_ y / x ]_ C )
14 13 fmpt 
 |-  ( A. y e. A [_ y / x ]_ C e. B <-> F : A --> B )
15 10 14 bitri 
 |-  ( A. x e. A C e. B <-> F : A --> B )