This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 “ 𝐵 ) )