Theorem nfaltop

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

	Ref	Expression
Hypotheses	nfaltop.1	$$⊢\underset{\_}{Ⅎ}xA$$
	nfaltop.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	nfaltop	$$⊢\underset{\_}{Ⅎ}x⟪A,B⟫$$

Proof

Step	Hyp	Ref	Expression
1		nfaltop.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfaltop.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-altop	$$⊢⟪A,B⟫=\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$
4	1	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{A\right\}$$
5	2	nfsn	$$⊢\underset{\_}{Ⅎ}x\left\{B\right\}$$
6	1 5	nfpr	$$⊢\underset{\_}{Ⅎ}x\left\{A,\left\{B\right\}\right\}$$
7	4 6	nfpr	$$⊢\underset{\_}{Ⅎ}x\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$
8	3 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}x⟪A,B⟫$$