Colors of
variables: wff setvar class |
Syntax hints: ↔
wb 176 = wceq 1642
{copab 4623 |
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-an 360
df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-opab 4624 |
This theorem is referenced by: df1st2
4739 dfsset2
4744 dfco1
4749 dfsi2
4752 fconstopab
4816 xpundi
4833 xpundir
4834 inxp
4864 opabbi2i
4867 cnvco
4895 resopab
5000 opabresid
5004 cnvi
5033 cnvun
5034 cnvxp
5044 coundi
5083 coundir
5084 df2nd2
5112 fvopabg
5392 cbvoprab1
5568 cbvoprab12
5570 dmoprabss
5576 resoprab
5582 fnov
5592 ov6g
5601 mpt2mptx
5709 mptv
5719 scancan
6332 |