Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1540
∈ wcel 2105 ⟨cop 4634 Rel wrel 5681 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-ext 2702 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 df-opab 5211 df-xp 5682 df-rel 5683 |
This theorem is referenced by: eqbrriv
5791 inopab
5829 difopab
5830 difopabOLD
5831 dfres2
6041 restidsing
6052 cnvopab
6138 cnvdif
6143 difxp
6163 cnvcnvsn
6218 dfco2
6244 coiun
6255 co02
6259 coass
6264 ressn
6284 ovoliunlem1
25252 h2hlm
30501 cnvco1
35034 cnvco2
35035 inxprnres
37465 cnviun
42704 coiun1
42706 |