Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∧ wa 397
= wceq 1542 ×
cxp 5675 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-opab 5212 df-xp 5683 |
This theorem is referenced by: xpeq12i
5705 xpeq12d
5708 xpid11
5932 xp11
6175 infxpenlem
10008 fpwwe2lem4
10629 pwfseqlem4a
10656 pwfseqlem4
10657 pwfseqlem5
10658 pwfseq
10659 pwsval
17432 mamufval
21887 mvmulfval
22044 txtopon
23095 txbasval
23110 txindislem
23137 ismet
23829 isxmet
23830 shsval
30565 sat1el2xp
34370 bj-imdirvallem
36061 prdsbnd2
36663 ismgmOLD
36718 opidon2OLD
36722 ttac
41775 rfovd
42752 fsovrfovd
42760 sblpnf
43069 |