Colors of
variables: wff setvar class |
Syntax hints: →
wi 4 ↔ wb 176
= wceq 1642 ∈ wcel 1710 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675
ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions:
df-bi 177 df-or 359
df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-v 2862 |
This theorem is referenced by: vtoclbg
2916 ceqex
2970 moeq3
3014 mo2icl
3016 sbctt
3109 sbcnestgf
3184 csbing
3463 csbifg
3691 prnzg
3837 sneqrg
3875 unisng
3909 snex
4112 snel1cg
4142 xpkvexg
4286 cnvkexg
4287 p6exg
4291 sikexg
4297 ins2kexg
4306 ins3kexg
4307 iota5
4360 csbiotag
4372 ssfin
4471 csbopabg
4638 vtoclr
4817 csbima12g
4956 dmsnopg
5067 fconstg
5252 fvelimab
5371 fvi
5443 csbovg
5553 trtxp
5782 oqelins4
5795 fnfullfunlem1
5857 fvfullfun
5865 fundmeng
6045 df1c3g
6142 sbthlem2
6205 frecxp
6315 frecxpg
6316 |