Colors of
variables: wff
setvar class |
Syntax hints:
β wi 4 β wcel 2105
β wne 2940 βwral 3061 β wss 3898
β
c0 4269 π«
cpw 4547 β© cint 4894 βcfv 6479
Moorecmre 17388 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-sep 5243 ax-nul 5250 ax-pow 5308 ax-pr 5372 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ral 3062 df-rex 3071 df-rab 3404 df-v 3443 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-nul 4270 df-if 4474 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4853 df-br 5093 df-opab 5155 df-mpt 5176 df-id 5518 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-iota 6431 df-fun 6481 df-fv 6487 df-mre 17392 |
This theorem is referenced by: mress
17399 mrerintcl
17403 mreuni
17406 mremre
17410 isacs2
17459 mreacs
17464 isacs3lem
18357 dmdprdd
19697 dprdfeq0
19720 dprdss
19727 dprdz
19728 subgdmdprd
19732 subgdprd
19733 dprd2dlem1
19739 dprd2da
19740 dmdprdsplit2lem
19743 mretopd
22349 ismrc
40785 |