This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ Ⅎ 𝑥 ( 𝐴 ⊔ 𝐵 )