Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 394
= wceq 1539 ∈
wcel 2104 ∀wral 3059
Xcixp 8893 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-ext 2701 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-ral 3060 df-v 3474 df-in 3954 df-ss 3964 df-ixp 8894 |
This theorem is referenced by: ixpeq2dv
8909 dfac9
10133 xpsrnbas
17521 funcpropd
17855 natpropd
17933 prdsmgp
20045 frlmip
21552 elptr2
23298 dfac14
23342 xkoptsub
23378 prdsxmslem2
24258 rrxip
25138 ptrest
36790 prdsbnd2
36966 hoidmvlelem3
45611 ovnhoilem1
45615 ovnhoilem2
45616 hoicoto2
45619 ovnlecvr2
45624 ovncvr2
45625 ovnovollem1
45670 ovnovollem2
45671 hoimbl2
45679 vonhoire
45686 iccvonmbllem
45692 vonioolem2
45695 vonicclem2
45698 vonn0ioo2
45704 vonn0icc2
45706 |