Theorem nfdju

Description: Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022)

	Ref	Expression
Hypotheses	nfdju.1	⊢ Ⅎ 𝑥 𝐴
	nfdju.2	⊢ Ⅎ 𝑥 𝐵
Assertion	nfdju	⊢ Ⅎ 𝑥 ( 𝐴 ⊔ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfdju.1	⊢ Ⅎ 𝑥 𝐴
2		nfdju.2	⊢ Ⅎ 𝑥 𝐵
3		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
4		nfcv	⊢ Ⅎ 𝑥 { ∅ }
5	4 1	nfxp	⊢ Ⅎ 𝑥 ( { ∅ } × 𝐴 )
6		nfcv	⊢ Ⅎ 𝑥 { 1o }
7	6 2	nfxp	⊢ Ⅎ 𝑥 ( { 1o } × 𝐵 )
8	5 7	nfun	⊢ Ⅎ 𝑥 ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
9	3 8	nfcxfr	⊢ Ⅎ 𝑥 ( 𝐴 ⊔ 𝐵 )