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 ⊢ φ → Ⅎ _ x A
nfimad.3 ⊢ φ → Ⅎ _ x B
Assertion nfimad ⊢ φ → Ⅎ _ x A B

Proof

Step Hyp Ref Expression
1 nfimad.2 ⊢ φ → Ⅎ _ x A
2 nfimad.3 ⊢ φ → Ⅎ _ x B
3 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ A
4 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ B
5 3 4 nfima ⊢ Ⅎ _ x z | ∀ x z ∈ A z | ∀ x z ∈ B
6 nfnfc1 ⊢ Ⅎ x Ⅎ _ x A
7 nfnfc1 ⊢ Ⅎ x Ⅎ _ x B
8 6 7 nfan ⊢ Ⅎ x Ⅎ _ x A ∧ Ⅎ _ x B
9 abidnf ⊢ Ⅎ _ x A → z | ∀ x z ∈ A = A
10 9 imaeq1d ⊢ Ⅎ _ x A → z | ∀ x z ∈ A z | ∀ x z ∈ B = A z | ∀ x z ∈ B
11 abidnf ⊢ Ⅎ _ x B → z | ∀ x z ∈ B = B
12 11 imaeq2d ⊢ Ⅎ _ x B → A z | ∀ x z ∈ B = A B
13 10 12 sylan9eq ⊢ Ⅎ _ x A ∧ Ⅎ _ x B → z | ∀ x z ∈ A z | ∀ x z ∈ B = A B
14 8 13 nfceqdf ⊢ Ⅎ _ x A ∧ Ⅎ _ x B → Ⅎ _ x z | ∀ x z ∈ A z | ∀ x z ∈ B ↔ Ⅎ _ x A B
15 1 2 14 syl2anc ⊢ φ → Ⅎ _ x z | ∀ x z ∈ A z | ∀ x z ∈ B ↔ Ⅎ _ x A B
16 5 15 mpbii ⊢ φ → Ⅎ _ x A B