HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem xpundi 4061
Description: Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52.
Assertion
Ref Expression
xpundi

Proof of Theorem xpundi
StepHypRef Expression
1 elun 2770 . . . . . 6
21anbi2i 670 . . . . 5
3 andi 800 . . . . 5
42, 3bitri 237 . . . 4
54opabbii 3417 . . 3
6 unopab 3426 . . 3
75, 6eqtr4i 1940 . 2
8 df-xp 4009 . 2
9 df-xp 4009 . . 3
10 df-xp 4009 . . 3
119, 10uneq12i 2781 . 2
127, 8, 113eqtr4i 1947 1
Colors of variables: wff set class
Syntax hints:   wo 355   wa 356   wceq 1413   wcel 1415   cun 2630  copab 3412   cxp 3993
This theorem is referenced by:  xpun 4066  xp2cda 6463  xpcdaen 6466  unctb 6675  alephadd 6679
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-ex 1335  df-sb 1590  df-clab 1905  df-cleq 1910  df-clel 1913  df-v 2324  df-un 2637  df-opab 3413  df-xp 4009
Copyright terms: Public domain