Metamath Proof Explorer


Theorem nfmpt

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

Ref Expression
Hypotheses nfmpt.1 𝑥 𝐴
nfmpt.2 𝑥 𝐵
Assertion nfmpt 𝑥 ( 𝑦𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 nfmpt.1 𝑥 𝐴
2 nfmpt.2 𝑥 𝐵
3 df-mpt ( 𝑦𝐴𝐵 ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦𝐴𝑧 = 𝐵 ) }
4 1 nfcri 𝑥 𝑦𝐴
5 2 nfeq2 𝑥 𝑧 = 𝐵
6 4 5 nfan 𝑥 ( 𝑦𝐴𝑧 = 𝐵 )
7 6 nfopab 𝑥 { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦𝐴𝑧 = 𝐵 ) }
8 3 7 nfcxfr 𝑥 ( 𝑦𝐴𝐵 )