Metamath Proof Explorer


Theorem nfima

Description: Bound-variable hypothesis builder for image. (Contributed by NM, 30-Dec-1996) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Hypotheses nfima.1
|- F/_ x A
nfima.2
|- F/_ x B
Assertion nfima
|- F/_ x ( A " B )

Proof

Step Hyp Ref Expression
1 nfima.1
 |-  F/_ x A
2 nfima.2
 |-  F/_ x B
3 df-ima
 |-  ( A " B ) = ran ( A |` B )
4 1 2 nfres
 |-  F/_ x ( A |` B )
5 4 nfrn
 |-  F/_ x ran ( A |` B )
6 3 5 nfcxfr
 |-  F/_ x ( A " B )