Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 397 ∈
wcel 2107 ≠ wne 2941
∀wral 3062 ∃wrex 3071 ⊆ wss 3949
∅c0 4323 class class class wbr 5149
Fr wfr 5629 |
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 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-v 3477 df-dif 3952 df-in 3956 df-ss 3966 df-pw 4605 df-sn 4630 df-fr 5632 |
This theorem is referenced by: frc
5643 fr2nr
5655 frminex
5657 wereu
5673 wereu2
5674 frpomin
6342 fr3nr
7759 frfi
9288 fimax2g
9289 fimin2g
9492 wofib
9540 wemapso
9546 wemapso2lem
9547 noinfep
9655 cflim2
10258 isfin1-3
10381 fin12
10408 fpwwe2lem11
10636 fpwwe2lem12
10637 fpwwe2
10638 bnj110
33869 frinfm
36603 fdc
36613 fnwe2lem2
41793 |