Theorem nfrel

Description: Bound-variable hypothesis builder for a relation. (Contributed by NM, 31-Jan-2004) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypothesis	nfrel.1	|- F/_ x A
Assertion	nfrel	|- F/ x Rel A

Proof

Step	Hyp	Ref	Expression
1		nfrel.1	|- F/_ x A
2		df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )
3		nfcv	|- F/_ x ( _V X. _V )
4	1 3	nfss	|- F/ x A C_ ( _V X. _V )
5	2 4	nfxfr	|- F/ x Rel A