Colors of
variables: wff set class |
Syntax hints: wi 4
wa 104
wceq 1351
weu 2022
wcel 2144
wral 2451
copab 4055 wfn 5200 |
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-io 707
ax-5 1443 ax-7 1444 ax-gen 1445 ax-ie1 1489 ax-ie2 1490 ax-8 1500 ax-10 1501 ax-11 1502 ax-i12 1503 ax-bndl 1505 ax-4 1506 ax-17 1522 ax-i9 1526 ax-ial 1530 ax-i5r 1531 ax-14 2147 ax-ext 2155 ax-sep 4113 ax-pow 4166 ax-pr 4200 |
This theorem depends on definitions:
df-bi 117 df-3an 978 df-tru 1354 df-nf 1457 df-sb 1759 df-eu 2025 df-mo 2026 df-clab 2160 df-cleq 2166 df-clel 2169 df-nfc 2304 df-ral 2456 df-rex 2457 df-v 2735 df-un 3128 df-in 3130 df-ss 3137 df-pw 3571 df-sn 3592 df-pr 3593 df-op 3595 df-br 3996 df-opab 4057 df-id 4284 df-xp 4623 df-rel 4624 df-cnv 4625 df-co 4626 df-dm 4627 df-fun 5207 df-fn 5208 |
This theorem is referenced by: fvopab3g
5578 |