Colors of
variables: wff
setvar class |
Syntax hints:
∩ cin 3910 ⊆ wss 3911
{csn 4587 ◡ccnv 5633
“ cima 5637 Predcpred 6253 |
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-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3446 df-in 3918 df-ss 3928 df-pred 6254 |
This theorem is referenced by: frpoins3xpg
8073 frpoins3xp3g
8074 xpord2pred
8078 xpord3pred
8085 fpr3g
8217 frrlem4
8221 frrlem13
8230 fpr1
8235 wfr3g
8254 wfrlem4OLD
8259 wfrlem10OLD
8265 ttrclselem1
9666 frmin
9690 frr3g
9697 frr1
9700 nummin
33752 wsuclem
34456 |