Colors of
variables: wff
setvar class |
Syntax hints:
∩ cin 3947 ⊆ wss 3948
{csn 4628 ◡ccnv 5675
“ cima 5679 Predcpred 6299 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-v 3476 df-in 3955 df-ss 3965 df-pred 6300 |
This theorem is referenced by: frpoins3xpg
8125 frpoins3xp3g
8126 xpord2pred
8130 xpord3pred
8137 fpr3g
8269 frrlem4
8273 frrlem13
8282 fpr1
8287 wfr3g
8306 wfrlem4OLD
8311 wfrlem10OLD
8317 ttrclselem1
9719 frmin
9743 frr3g
9750 frr1
9753 nummin
34089 wsuclem
34792 |