Colors of
variables: wff
setvar class |
Syntax hints: -> wi 4 <-> wb 184
A. wal 1393 e. wcel 1818 { cab 2442
A. wral 2807 E. wrex 2808 cvv 3109
C_ wss 3475 U_ ciun 4330 X. cxp 5002
Rel wrel 5009 |
This theorem is referenced by: reluni
5130 eliunxp
5145 opeliunxp2
5146 dfco2
5511 coiun
5522 fvn0ssdmfun
6022 fsumcom2
13589 fprodcom2
13788 imasaddfnlem
14925 imasvscafn
14934 gsum2d2lem
17001 gsum2d2
17002 gsumcom2
17003 dprd2d2
17093 cnextrel
20563 reldv
22274 dfcnv2
27517 cvmliftlem1
28730 eliunxp2
32923 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704
ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 |
This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ral 2812 df-rex 2813 df-v 3111 df-in 3482 df-ss 3489 df-iun 4332 df-rel 5011 |