Theorem nfaltop

Description: Bound-variable hypothesis builder for alternate ordered pairs. (Contributed by Scott Fenton, 25-Sep-2015)

	Ref	Expression
Hypotheses	nfaltop.1	|- F/_ x A
	nfaltop.2	|- F/_ x B
Assertion	nfaltop	|- F/_ x << A , B >>

Proof

Step	Hyp	Ref	Expression
1		nfaltop.1	|- F/_ x A
2		nfaltop.2	|- F/_ x B
3		df-altop	|- << A , B >> = { { A } , { A , { B } } }
4	1	nfsn	|- F/_ x { A }
5	2	nfsn	|- F/_ x { B }
6	1 5	nfpr	|- F/_ x { A , { B } }
7	4 6	nfpr	|- F/_ x { { A } , { A , { B } } }
8	3 7	nfcxfr	|- F/_ x << A , B >>