Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ◡ccnv 4626
Fun wfun 5211 ⟶wf 5213 –1-1→wf1 5214 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 |
This theorem depends on definitions:
df-bi 117 df-f1 5222 |
This theorem is referenced by: f1rn
5423 f1fn
5424 f1ss
5428 f1ssres
5431 f1of
5462 dff1o5
5471 fsnd
5505 cocan1
5788 f1o2ndf1
6229 brdomg
6748 f1dom2g
6756 f1domg
6758 dom3d
6774 f1imaen2g
6793 2dom
6805 xpdom2
6831 dom0
6838 phplem4dom
6862 isinfinf
6897 infm
6904 updjudhcoinlf
7079 updjudhcoinrg
7080 casef1
7089 djudom
7092 difinfsnlem
7098 difinfsn
7099 fihashf1rn
10768 ennnfonelemrn
12420 reeff1o
14197 pwle2
14751 |