Metamath Proof Explorer
Description: Boundvariable hypothesis builder for binary relation. (Contributed by NM, 1Sep1999) (Revised by Mario Carneiro, 14Oct2016)


Ref 
Expression 

Hypotheses 
nfbr.1 
 F/_ x A 


nfbr.2 
 F/_ x R 


nfbr.3 
 F/_ x B 

Assertion 
nfbr 
 F/ x A R B 
Proof
Step 
Hyp 
Ref 
Expression 
1 

nfbr.1 
 F/_ x A 
2 

nfbr.2 
 F/_ x R 
3 

nfbr.3 
 F/_ x B 
4 
1

a1i 
 ( T. > F/_ x A ) 
5 
2

a1i 
 ( T. > F/_ x R ) 
6 
3

a1i 
 ( T. > F/_ x B ) 
7 
4 5 6

nfbrd 
 ( T. > F/ x A R B ) 
8 
7

mptru 
 F/ x A R B 