Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 397 ∧
w3a 1088 ∈ wcel 2107
class class class wbr 5149 Po wpo 5587 |
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-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-po 5589 |
This theorem is referenced by: po2nr
5603 po3nr
5604 pofun
5607 sotr
5613 poltletr
6134 frpomin
6342 poxp
8114 poxp2
8129 poxp3
8136 poseq
8144 fprlem2
8286 frfi
9288 wemaplem2
9542 sornom
10272 zorn2lem7
10497 pospo
18298 pocnv
34733 seqpo
36615 oneptr
42004 |