Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Vcvv 3448
∪ cun 3913 {csn 4591
{cpr 4593 {ctp 4595 |
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 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2708 ax-sep 5261 ax-nul 5268 ax-pr 5389 ax-un 7677 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-sn 4592 df-pr 4594 df-tp 4596 df-uni 4871 |
This theorem is referenced by: fr3nr
7711 en3lp
9557 prdsval
17344 imasval
17400 fnfuc
17839 fucval
17853 setcval
17970 catcval
17993 estrcval
18018 estrreslem1
18031 estrreslem1OLD
18032 estrres
18034 fnxpc
18071 xpcval
18072 efmnd
18687 xrsex
20828 psrval
21333 om1val
24409 idlsrgval
32285 signswbase
33206 signswplusg
33207 ldualset
37616 erngset
39292 erngset-rN
39300 dvaset
39497 dvhset
39573 hlhilset
40426 rabren3dioph
41167 mendval
41539 clsk1indlem4
42390 clsk1indlem1
42391 rngcvalALTV
46333 ringcvalALTV
46379 lmod1zrnlvec
46649 mndtcval
47179 |