Theorem nfbr

Description: Bound-variable hypothesis builder for binary relation. (Contributed by NM, 1-Sep-1999) (Revised by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nfbr.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfbr.2	$$⊢\underset{\_}{Ⅎ}xR$$
	nfbr.3	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfbr	$$⊢ℲxARB$$

Proof

Step	Hyp	Ref	Expression
1		nfbr.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfbr.2	$$⊢\underset{\_}{Ⅎ}xR$$
3		nfbr.3	$$⊢\underset{\_}{Ⅎ}xB$$
4	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
5	2	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xR$$
6	3	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xB$$
7	4 5 6	nfbrd	$$⊢\top \to ℲxARB$$
8	7	mptru	$$⊢ℲxARB$$