Theorem nffvd

Description: Deduction version of bound-variable hypothesis builder nffv . (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nffvd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
	nffvd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nffvd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		nffvd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
2		nffvd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 }
4		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 }
5	3 4	nffv	⊢ Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } ‘ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } )
6		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐹
7		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
8	6 7	nfan	⊢ Ⅎ 𝑥 ( Ⅎ 𝑥 𝐹 ∧ Ⅎ 𝑥 𝐴 )
9		abidnf	⊢ ( Ⅎ 𝑥 𝐹 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } = 𝐹 )
10	9	adantr	⊢ ( ( Ⅎ 𝑥 𝐹 ∧ Ⅎ 𝑥 𝐴 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } = 𝐹 )
11		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
12	11	adantl	⊢ ( ( Ⅎ 𝑥 𝐹 ∧ Ⅎ 𝑥 𝐴 ) → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
13	10 12	fveq12d	⊢ ( ( Ⅎ 𝑥 𝐹 ∧ Ⅎ 𝑥 𝐴 ) → ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } ‘ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } ) = ( 𝐹 ‘ 𝐴 ) )
14	8 13	nfceqdf	⊢ ( ( Ⅎ 𝑥 𝐹 ∧ Ⅎ 𝑥 𝐴 ) → ( Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } ‘ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } ) ↔ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 ) ) )
15	1 2 14	syl2anc	⊢ ( 𝜑 → ( Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐹 } ‘ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } ) ↔ Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 ) ) )
16	5 15	mpbii	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐹 ‘ 𝐴 ) )