Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2098
∪ cun 3938 ⊆
wss 3940 𝒫 cpw 4594
× cxp 5664 WUnicwun 10691 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-pw 4596 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-opab 5201 df-tr 5256 df-xp 5672 df-rel 5673 df-wun 10693 |
This theorem is referenced by: wunpm
10716 wuncnv
10721 wunco
10724 wuntpos
10725 tskxp
10778 wuncn
11161 wunfunc
17850 wunfuncOLD
17851 wunnat
17909 wunnatOLD
17910 catcoppccl
18069 catcoppcclOLD
18070 catcfuccl
18071 catcfucclOLD
18072 catcxpccl
18161 catcxpcclOLD
18162 |