Theorem nfdju

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

	Ref	Expression
Hypotheses	nfdju.1	|- F/_ x A
	nfdju.2	|- F/_ x B
Assertion	nfdju	|- F/_ x ( A |_| B )

Proof

Step	Hyp	Ref	Expression
1		nfdju.1	|- F/_ x A
2		nfdju.2	|- F/_ x B
3		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
4		nfcv	|- F/_ x { (/) }
5	4 1	nfxp	|- F/_ x ( { (/) } X. A )
6		nfcv	|- F/_ x { 1o }
7	6 2	nfxp	|- F/_ x ( { 1o } X. B )
8	5 7	nfun	|- F/_ x ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
9	3 8	nfcxfr	|- F/_ x ( A |_| B )