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

Metamath Proof Explorer

Theorem nfbrd

Description: Deduction version of bound-variable hypothesis builder nfbr . (Contributed by NM, 13-Dec-2005) (Revised by Mario Carneiro, 14-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nfbrd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		nfbrd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝑅 )
3		nfbrd.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
4		df-br	⊢ ( 𝐴 𝑅 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
5	1 3	nfopd	⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ )
6	5 2	nfeld	⊢ ( 𝜑 → Ⅎ 𝑥 ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝑅 )
7	4 6	nfxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 𝑅 𝐵 )