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	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfbrd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xR$$
	nfbrd.4	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfbrd	$$⊢\phi \to ℲxARB$$

Proof

Step	Hyp	Ref	Expression
1		nfbrd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfbrd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xR$$
3		nfbrd.4	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
4		df-br	$$⊢ARB\leftrightarrow ⟨A,B⟩\in R$$
5	1 3	nfopd	$$⊢\phi \to \underset{\_}{Ⅎ}x⟨A,B⟩$$
6	5 2	nfeld	$$⊢\phi \to Ⅎx⟨A,B⟩\in R$$
7	4 6	nfxfrd	$$⊢\phi \to ℲxARB$$