Colors of
variables: wff set class |
Syntax hints: wcel 2146
cvv 2735
cpr 3590 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709
ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-v 2737 df-un 3131 df-sn 3595 df-pr 3596 |
This theorem is referenced by: prid2
3696 prnz
3711 preqr1
3764 preq12b
3766 prel12
3767 opi1
4226 opeluu
4444 onsucelsucexmidlem1
4521 regexmidlem1
4526 reg2exmidlema
4527 opthreg
4549 ordtri2or2exmid
4564 ontri2orexmidim
4565 dmrnssfld
4883 funopg
5242 acexmidlemb
5857 0lt2o
6432 2dom
6795 unfiexmid
6907 djuss
7059 exmidomni
7130 exmidonfinlem
7182 exmidaclem
7197 reelprrecn
7921 pnfxr
7984 sup3exmid
8885 lgsdir2lem3
13924 bdop
14109 2o01f
14228 iswomni0
14282 |