Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
≠ wne 2941 ∅c0 4323 {cpr 4631 |
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 2704 |
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 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-dif 3952 df-un 3954 df-nul 4324 df-sn 4630 df-pr 4632 |
This theorem is referenced by: preqsnd
4860 0nelop
5497 fr2nr
5655 mreincl
17543 subrgin
20343 lssincl
20576 incld
22547 umgrnloopv
28366 upgr1elem
28372 usgrnloopvALT
28458 difelsiga
33131 inelpisys
33152 inidl
36898 coss0
37349 pmapmeet
38644 diameetN
39927 dihmeetlem2N
40170 dihmeetcN
40173 dihmeet
40214 subrngin
46740 |