Metamath Proof Explorer

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 ⊢ φ → Ⅎ _ x F
nffvd.3 ⊢ φ → Ⅎ _ x A
Assertion nffvd ⊢ φ → Ⅎ _ x F ⁡ A

Proof

Step Hyp Ref Expression
1 nffvd.2 ⊢ φ → Ⅎ _ x F
2 nffvd.3 ⊢ φ → Ⅎ _ x A
3 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ F
4 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ A
5 3 4 nffv ⊢ Ⅎ _ x z | ∀ x z ∈ F ⁡ z | ∀ x z ∈ A
6 nfnfc1 ⊢ Ⅎ x Ⅎ _ x F
7 nfnfc1 ⊢ Ⅎ x Ⅎ _ x A
8 6 7 nfan ⊢ Ⅎ x Ⅎ _ x F ∧ Ⅎ _ x A
9 abidnf ⊢ Ⅎ _ x F → z | ∀ x z ∈ F = F
10 9 adantr ⊢ Ⅎ _ x F ∧ Ⅎ _ x A → z | ∀ x z ∈ F = F
11 abidnf ⊢ Ⅎ _ x A → z | ∀ x z ∈ A = A
12 11 adantl ⊢ Ⅎ _ x F ∧ Ⅎ _ x A → z | ∀ x z ∈ A = A
13 10 12 fveq12d ⊢ Ⅎ _ x F ∧ Ⅎ _ x A → z | ∀ x z ∈ F ⁡ z | ∀ x z ∈ A = F ⁡ A
14 8 13 nfceqdf ⊢ Ⅎ _ x F ∧ Ⅎ _ x A → Ⅎ _ x z | ∀ x z ∈ F ⁡ z | ∀ x z ∈ A ↔ Ⅎ _ x F ⁡ A
15 1 2 14 syl2anc ⊢ φ → Ⅎ _ x z | ∀ x z ∈ F ⁡ z | ∀ x z ∈ A ↔ Ⅎ _ x F ⁡ A
16 5 15 mpbii ⊢ φ → Ⅎ _ x F ⁡ A