This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfsn

Description: Bound-variable hypothesis builder for singletons. (Contributed by NM, 14-Nov-1995)

Ref Expression
Hypothesis nfsn.1 ⊢ Ⅎ _ x A
Assertion nfsn ⊢ Ⅎ _ x A

Proof

Step Hyp Ref Expression
1 nfsn.1 ⊢ Ⅎ _ x A
2 dfsn2 ⊢ A = A A
3 1 1 nfpr ⊢ Ⅎ _ x A A
4 2 3 nfcxfr ⊢ Ⅎ _ x A