Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1539
∈ wcel 2104 ⟨cop 4633 Rel wrel 5680 |
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-v 3474 df-in 3954 df-ss 3964 df-opab 5210 df-xp 5681 df-rel 5682 |
This theorem is referenced by: eqbrriv
5790 inopab
5828 difopab
5829 difopabOLD
5830 dfres2
6040 restidsing
6051 cnvopab
6137 cnvdif
6142 difxp
6162 cnvcnvsn
6217 dfco2
6243 coiun
6254 co02
6258 coass
6263 ressn
6283 ovoliunlem1
25251 h2hlm
30500 cnvco1
35033 cnvco2
35034 inxprnres
37464 cnviun
42703 coiun1
42705 |