Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1542
∈ wcel 2107 ⟨cop 4635 Rel wrel 5682 |
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-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-opab 5212 df-xp 5683 df-rel 5684 |
This theorem is referenced by: eqbrriv
5792 inopab
5830 difopab
5831 difopabOLD
5832 dfres2
6042 restidsing
6053 cnvopab
6139 cnvdif
6144 difxp
6164 cnvcnvsn
6219 dfco2
6245 coiun
6256 co02
6260 coass
6265 ressn
6285 ovoliunlem1
25019 h2hlm
30233 cnvco1
34729 cnvco2
34730 inxprnres
37161 cnviun
42401 coiun1
42403 |