Theorem nfaltop

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

	Ref	Expression
Hypotheses	nfaltop.1	⊢ Ⅎ 𝑥 𝐴
	nfaltop.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfaltop	⊢ Ⅎ 𝑥 ⟪ 𝐴 , 𝐵 ⟫

Proof

Step	Hyp	Ref	Expression
1		nfaltop.1	⊢ Ⅎ 𝑥 𝐴
2		nfaltop.2	⊢ Ⅎ 𝑥 𝐵
3		df-altop	⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }
4	1	nfsn	⊢ Ⅎ 𝑥 { 𝐴 }
5	2	nfsn	⊢ Ⅎ 𝑥 { 𝐵 }
6	1 5	nfpr	⊢ Ⅎ 𝑥 { 𝐴 , { 𝐵 } }
7	4 6	nfpr	⊢ Ⅎ 𝑥 { { 𝐴 } , { 𝐴 , { 𝐵 } } }
8	3 7	nfcxfr	⊢ Ⅎ 𝑥 ⟪ 𝐴 , 𝐵 ⟫