Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2104
∅c0 4323 ⟨cop 4635 class class class wbr 5149 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-dif 3952 df-nul 4324 df-br 5150 |
This theorem is referenced by: sbcbr123
5203 sbcbr
5204 cnv0
6141 co02
6260 fvmptopabOLD
7468 brfvopab
7470 0we1
8510 brdom3
10527 canthwe
10650 relexpindlem
15016 join0
18364 meet0
18365 acycgr0v
34435 prclisacycgr
34438 disjALTV0
37929 brnonrel
42644 upwlkbprop
46816 |