Metamath Proof Explorer


Theorem fmptf

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fmptf.1 𝑥 𝐵
fmptf.2 𝐹 = ( 𝑥𝐴𝐶 )
Assertion fmptf ( ∀ 𝑥𝐴 𝐶𝐵𝐹 : 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 fmptf.1 𝑥 𝐵
2 fmptf.2 𝐹 = ( 𝑥𝐴𝐶 )
3 nfv 𝑦 𝐶𝐵
4 nfcsb1v 𝑥 𝑦 / 𝑥 𝐶
5 4 1 nfel 𝑥 𝑦 / 𝑥 𝐶𝐵
6 csbeq1a ( 𝑥 = 𝑦𝐶 = 𝑦 / 𝑥 𝐶 )
7 6 eleq1d ( 𝑥 = 𝑦 → ( 𝐶𝐵 𝑦 / 𝑥 𝐶𝐵 ) )
8 3 5 7 cbvralw ( ∀ 𝑥𝐴 𝐶𝐵 ↔ ∀ 𝑦𝐴 𝑦 / 𝑥 𝐶𝐵 )
9 nfcv 𝑦 𝐶
10 9 4 6 cbvmpt ( 𝑥𝐴𝐶 ) = ( 𝑦𝐴 𝑦 / 𝑥 𝐶 )
11 2 10 eqtri 𝐹 = ( 𝑦𝐴 𝑦 / 𝑥 𝐶 )
12 11 fmpt ( ∀ 𝑦𝐴 𝑦 / 𝑥 𝐶𝐵𝐹 : 𝐴𝐵 )
13 8 12 bitri ( ∀ 𝑥𝐴 𝐶𝐵𝐹 : 𝐴𝐵 )