Colors of
variables: wff
setvar class |
Syntax hints: -. wn 3 <-> wb 184
/\ wa 369 e. wcel 1757 \ cdif 3407
C_ wss 3410 con0 4801 suc csuc 4803 c1o 6997
c2o 6998 |
This theorem is referenced by: dif20el
7029 oeordi
7110 oewordi
7114 oaabs2
7168 omabs
7170 cnfcom3clem
8023 cnfcom3clemOLD
8031 infxpenc2lem1
8270 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671
ax-6 1709 ax-7 1729 ax-8 1759
ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-sep 4495 ax-nul 4503 ax-pr 4613 ax-un 6456 |
This theorem depends on definitions:
df-bi 185 df-or 370
df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-eu 2263 df-mo 2264 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-ral 2797 df-rex 2798 df-rab 2801 df-v 3054 df-sbc 3269 df-dif 3413 df-un 3415 df-in 3417 df-ss 3424 df-pss 3426 df-nul 3720 df-if 3874 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4174 df-br 4375 df-opab 4433 df-tr 4468 df-eprel 4714 df-po 4723 df-so 4724 df-fr 4761 df-we 4763 df-ord 4804 df-on 4805 df-suc 4807 df-1o 7004 df-2o 7005 |