Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
= wceq 1533 –1-1-onto→wf1o 6532 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-ext 2695 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-br 5139 df-opab 5201 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 |
This theorem is referenced by: f1orescnv
6838 f1osng
6864 f1ofvswap
7296 dif1en
9155 dif1enOLD
9157 cnfcomlem
9689 cnfcom2
9692 cnfcom3clem
9695 infxpenc
10008 infxpenc2lem2
10010 infxpenc2
10012 canthp1lem2
10643 pwfseqlem5
10653 pwfseq
10654 s2f1o
14863 s4f1o
14865 bitsf1ocnv
16381 yonffthlem
18234 grplactcnv
18958 eqgen
19093 znunithash
21420 tgpconncompeqg
23926 fcobijfs
32372 s2f1
32535 mgcf1o
32597 gsummpt2d
32628 indf1o
33477 subfacp1lem3
34628 subfacp1lem5
34630 ismrer1
37162 hvmap1o
41090 metakunt34
41477 |