Colors of
variables: wff set class |
Syntax hints:
↔ wb 105 = wceq 1353
{copab 4064 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448
ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-opab 4066 |
This theorem is referenced by: mptv
4101 fconstmpt
4674 xpundi
4683 xpundir
4684 inxp
4762 cnvco
4813 resopab
4952 opabresid
4961 cnvi
5034 cnvun
5035 cnvin
5037 cnvxp
5048 cnvcnv3
5079 coundi
5131 coundir
5132 mptun
5348 fvopab6
5613 cbvoprab1
5947 cbvoprab12
5949 dmoprabss
5957 mpomptx
5966 resoprab
5971 ov6g
6012 dfoprab3s
6191 dfoprab3
6192 dfoprab4
6193 mapsncnv
6695 xpcomco
6826 dmaddpq
7378 dmmulpq
7379 recmulnqg
7390 enq0enq
7430 ltrelxr
8018 ltxr
9775 shftidt2
10841 prdsex
12718 releqgg
13080 dvdsrzring
13496 lmfval
13695 lmbr
13716 cnmptid
13784 |