Theorem nfimad

Description: Deduction version of bound-variable hypothesis builder nfima . (Contributed by FL, 15-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nfimad.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfimad.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfimad	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nfimad.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfimad.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
3		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 }
4		nfaba1	⊢ Ⅎ 𝑥 { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 }
5	3 4	nfima	⊢ Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } )
6		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐴
7		nfnfc1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝐵
8	6 7	nfan	⊢ Ⅎ 𝑥 ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 )
9		abidnf	⊢ ( Ⅎ 𝑥 𝐴 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } = 𝐴 )
10	9	imaeq1d	⊢ ( Ⅎ 𝑥 𝐴 → ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) = ( 𝐴 “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) )
11		abidnf	⊢ ( Ⅎ 𝑥 𝐵 → { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } = 𝐵 )
12	11	imaeq2d	⊢ ( Ⅎ 𝑥 𝐵 → ( 𝐴 “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) = ( 𝐴 “ 𝐵 ) )
13	10 12	sylan9eq	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) = ( 𝐴 “ 𝐵 ) )
14	8 13	nfceqdf	⊢ ( ( Ⅎ 𝑥 𝐴 ∧ Ⅎ 𝑥 𝐵 ) → ( Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) ↔ Ⅎ 𝑥 ( 𝐴 “ 𝐵 ) ) )
15	1 2 14	syl2anc	⊢ ( 𝜑 → ( Ⅎ 𝑥 ( { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐴 } “ { 𝑧 ∣ ∀ 𝑥 𝑧 ∈ 𝐵 } ) ↔ Ⅎ 𝑥 ( 𝐴 “ 𝐵 ) ) )
16	5 15	mpbii	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 “ 𝐵 ) )