Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
nfovd
Metamath Proof Explorer
Description: Deduction version of bound-variable hypothesis builder nfov .
(Contributed by NM , 13-Dec-2005) (Proof shortened by Andrew Salmon , 22-Oct-2011)

Ref
Expression
Hypotheses
nfovd.2
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
nfovd.3
⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
nfovd.4
⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion
nfovd
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 ) )

Proof
Step
Hyp
Ref
Expression
1
nfovd.2
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2
nfovd.3
⊢ ( 𝜑 → Ⅎ 𝑥 𝐹 )
3
nfovd.4
⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
4
df-ov
⊢ ( 𝐴 𝐹 𝐵 ) = ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
5
1 3
nfopd
⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ )
6
2 5
nffvd
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐹 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
7
4 6
nfcxfrd
⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝐴 𝐹 𝐵 ) )