Metamath Proof Explorer

Theorem nfopd

Description: Deduction version of bound-variable hypothesis builder nfop . This shows how the deduction version of a not-free theorem such as nfop can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008)

Ref Expression
Hypotheses nfopd.2 ⊢ φ → Ⅎ _ x A
nfopd.3 ⊢ φ → Ⅎ _ x B
Assertion nfopd ⊢ φ → Ⅎ _ x A B

Proof

Step Hyp Ref Expression
1 nfopd.2 ⊢ φ → Ⅎ _ x A
2 nfopd.3 ⊢ φ → Ⅎ _ x B
3 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ A
4 nfaba1 ⊢ Ⅎ _ x z | ∀ x z ∈ B
5 3 4 nfop ⊢ Ⅎ _ 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 adantr ⊢ Ⅎ _ x A ∧ Ⅎ _ x B → z | ∀ x z ∈ A = A
11 abidnf ⊢ Ⅎ _ x B → z | ∀ x z ∈ B = B
12 11 adantl ⊢ Ⅎ _ x A ∧ Ⅎ _ x B → z | ∀ x z ∈ B = B
13 10 12 opeq12d ⊢ Ⅎ _ 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