Colors of
variables: wff set class |
Syntax hints:
→ wi 4 ◡ccnv 4625
Fun wfun 5210 ⟶wf 5212 –1-1→wf1 5213 |
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 5221 |
This theorem is referenced by: f1rn
5422 f1fn
5423 f1ss
5427 f1ssres
5430 f1of
5461 dff1o5
5470 fsnd
5504 cocan1
5787 f1o2ndf1
6228 brdomg
6747 f1dom2g
6755 f1domg
6757 dom3d
6773 f1imaen2g
6792 2dom
6804 xpdom2
6830 dom0
6837 phplem4dom
6861 isinfinf
6896 infm
6903 updjudhcoinlf
7078 updjudhcoinrg
7079 casef1
7088 djudom
7091 difinfsnlem
7097 difinfsn
7098 fihashf1rn
10767 ennnfonelemrn
12419 reeff1o
14164 pwle2
14718 |