Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 397 ∈
wcel 2107 ≠ wne 2944
∀wral 3065 ∃wrex 3074 ⊆ wss 3911
∅c0 4283 class class class wbr 5106
Fr wfr 5586 |
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 2708 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-v 3448 df-dif 3914 df-in 3918 df-ss 3928 df-pw 4563 df-sn 4588 df-fr 5589 |
This theorem is referenced by: frc
5600 fr2nr
5612 frminex
5614 wereu
5630 wereu2
5631 frpomin
6295 fr3nr
7707 frfi
9233 fimax2g
9234 fimin2g
9434 wofib
9482 wemapso
9488 wemapso2lem
9489 noinfep
9597 cflim2
10200 isfin1-3
10323 fin12
10350 fpwwe2lem11
10578 fpwwe2lem12
10579 fpwwe2
10580 bnj110
33473 frinfm
36197 fdc
36207 fnwe2lem2
41381 |