Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
= wceq 1542 Rel wrel 5643 |
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 2708 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3450 df-in 3922 df-ss 3932 df-rel 5645 |
This theorem is referenced by: dftpos3
8180 tposfo2
8185 tposf12
8187 relexp0rel
14929 relexprelg
14930 relexpreld
14932 relexpaddg
14945 imasaddfnlem
17417 imasvscafn
17426 cicer
17696 joindmss
18275 meetdmss
18289 mattpostpos
21819 cnextrel
23430 perpln1
27694 perpln2
27695 relfae
32886 satfrel
34001 dibvalrel
39655 dicvalrelN
39677 diclspsn
39686 dihvalrel
39771 dih1
39778 dihmeetlem4preN
39798 |