Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
= wceq 1540 ∈
wcel 2105 Vcvv 3441
class class class wbr 5089 {copab 5151 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-ext 2707 ax-sep 5240 ax-nul 5247 ax-pr 5369 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-sb 2067 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3404 df-v 3443 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4269 df-if 4473 df-sn 4573 df-pr 4575 df-op 4579 df-br 5090 df-opab 5152 |
This theorem is referenced by: opbrop
5709 f1oweALT
7875 frxp
8026 fnwelem
8031 poseq
8037 dftpos4
8123 dfac3
9970 axdc2lem
10297 brdom7disj
10380 brdom6disj
10381 ordpipq
10791 ltresr
10989 shftfn
14875 2shfti
14882 ishpg
27350 brcgr
27498 ex-opab
29025 br8d
31178 br8
33956 br6
33957 br4
33958 xpord2lem
34015 xpord3lem
34021 dfbigcup2
34292 brsegle
34501 heiborlem2
36068 |