Metamath Proof Explorer


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 _ x A
Assertion nfrel x Rel A

Proof

Step Hyp Ref Expression
1 nfrel.1 _ x A
2 df-rel Rel A A V × V
3 nfcv _ x V × V
4 1 3 nfss x A V × V
5 2 4 nfxfr x Rel A