Metamath Proof Explorer


Theorem fnmptif

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

Ref Expression
Hypotheses fnmptif.1 𝑥 𝐴
fnmptif.2 𝐵 ∈ V
fnmptif.3 𝐹 = ( 𝑥𝐴𝐵 )
Assertion fnmptif 𝐹 Fn 𝐴

Proof

Step Hyp Ref Expression
1 fnmptif.1 𝑥 𝐴
2 fnmptif.2 𝐵 ∈ V
3 fnmptif.3 𝐹 = ( 𝑥𝐴𝐵 )
4 2 rgenw 𝑥𝐴 𝐵 ∈ V
5 1 mptfnf ( ∀ 𝑥𝐴 𝐵 ∈ V ↔ ( 𝑥𝐴𝐵 ) Fn 𝐴 )
6 4 5 mpbi ( 𝑥𝐴𝐵 ) Fn 𝐴
7 3 fneq1i ( 𝐹 Fn 𝐴 ↔ ( 𝑥𝐴𝐵 ) Fn 𝐴 )
8 6 7 mpbir 𝐹 Fn 𝐴