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 | ⊢ Ⅎ 𝑥 𝐴 | |
| Assertion | nfrel | ⊢ Ⅎ 𝑥 Rel 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfrel.1 | ⊢ Ⅎ 𝑥 𝐴 | |
| 2 | df-rel | ⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) ) | |
| 3 | nfcv | ⊢ Ⅎ 𝑥 ( V × V ) | |
| 4 | 1 3 | nfss | ⊢ Ⅎ 𝑥 𝐴 ⊆ ( V × V ) |
| 5 | 2 4 | nfxfr | ⊢ Ⅎ 𝑥 Rel 𝐴 |