Colors of
variables: wff
setvar class |
Syntax hints: ¬ wn 3 → wi 4
↔ wb 205 ∧
wa 397 ∈ wcel 2107
⊆ wss 3948 Ord word 6361
Oncon0 6362 |
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 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 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-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-tr 5266 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-ord 6365 df-on 6366 |
This theorem is referenced by: oneqmini
6414 onmindif
6454 onint
7775 onnmin
7783 onmindif2
7792 dfom2
7854 ondif2
8499 oaword
8546 oawordeulem
8551 oaf1o
8560 odi
8576 omeulem1
8579 oeeulem
8598 oeeui
8599 nnmword
8630 cofonr
8670 naddel1
8683 naddss1
8685 domtriord
9120 sdomel
9121 onsdominel
9123 ordunifi
9290 cantnfp1lem3
9672 oemapvali
9676 cantnflem1b
9678 cantnflem1
9681 cnfcom3lem
9695 rankr1clem
9812 rankelb
9816 rankval3b
9818 rankr1a
9828 unbndrank
9834 rankxplim3
9873 cardne
9957 carden2b
9959 cardsdomel
9966 carddom2
9969 harcard
9970 domtri2
9981 infxpenlem
10005 alephord
10067 alephord3
10070 alephle
10080 dfac12k
10139 cflim2
10255 cofsmo
10261 cfsmolem
10262 isf32lem5
10349 pwcfsdom
10575 pwfseqlem3
10652 inar1
10767 om2uzlt2i
13913 sltval2
27149 sltres
27155 nosepssdm
27179 nolt02olem
27187 nolt02o
27188 nogt01o
27189 noetasuplem4
27229 noetainflem4
27233 nocvxminlem
27269 madebdaylemlrcut
27383 nummin
34083 onsuct0
35315 onint1
35323 onmaxnelsup
41958 onsupnmax
41963 onsupuni
41964 oninfint
41971 onsupmaxb
41974 onsupeqnmax
41982 oe0suclim
42013 cantnfresb
42060 cantnf2
42061 tfsconcatfv
42077 tfsnfin
42088 oadif1lem
42115 oadif1
42116 naddwordnexlem4
42138 ontric3g
42259 infordmin
42269 minregex
42271 alephiso3
42296 |