Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
∧ wa 396 ∈
wcel 2106 ≠ wne 2940
∀wral 3061 ∃wrex 3070 ⊆ wss 3947
∅c0 4321 class class class wbr 5147
Fr wfr 5627 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2703 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ne 2941 df-ral 3062 df-rex 3071 df-v 3476 df-dif 3950 df-in 3954 df-ss 3964 df-pw 4603 df-sn 4628 df-fr 5630 |
This theorem is referenced by: frc
5641 fr2nr
5653 frminex
5655 wereu
5671 wereu2
5672 frpomin
6338 fr3nr
7755 frfi
9284 fimax2g
9285 fimin2g
9488 wofib
9536 wemapso
9542 wemapso2lem
9543 noinfep
9651 cflim2
10254 isfin1-3
10377 fin12
10404 fpwwe2lem11
10632 fpwwe2lem12
10633 fpwwe2
10634 bnj110
33857 frinfm
36591 fdc
36601 fnwe2lem2
41778 |