Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfdju Structured version   Visualization version   GIF version

Theorem nfdju 9362
 Description: Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
Hypotheses
Ref Expression
nfdju.1 𝑥𝐴
nfdju.2 𝑥𝐵
Assertion
Ref Expression
nfdju 𝑥(𝐴𝐵)

Proof of Theorem nfdju
StepHypRef Expression
1 df-dju 9356 . 2 (𝐴𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
2 nfcv 2920 . . . 4 𝑥{∅}
3 nfdju.1 . . . 4 𝑥𝐴
42, 3nfxp 5558 . . 3 𝑥({∅} × 𝐴)
5 nfcv 2920 . . . 4 𝑥{1o}
6 nfdju.2 . . . 4 𝑥𝐵
75, 6nfxp 5558 . . 3 𝑥({1o} × 𝐵)
84, 7nfun 4071 . 2 𝑥(({∅} × 𝐴) ∪ ({1o} × 𝐵))
91, 8nfcxfr 2918 1 𝑥(𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnfc 2900   ∪ cun 3857  ∅c0 4226  {csn 4523   × cxp 5523  1oc1o 8106   ⊔ cdju 9353 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-un 3864  df-opab 5096  df-xp 5531  df-dju 9356 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator