![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inex1g | Structured version Visualization version Unicode version |
Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Ref | Expression |
---|---|
inex1g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 3638 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | eleq1d 2523 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3059 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 3 | inex1 4557 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 3118 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-v 3058 df-in 3422 |
This theorem is referenced by: dmresexg 5145 onin 5472 offval 6564 offval3 6813 onsdominel 7746 ssenen 7771 inelfi 7957 fiin 7961 tskwe 8409 dfac8b 8487 ac10ct 8490 infpwfien 8518 fictb 8700 canthnum 9099 gruina 9268 ressinbas 15233 ressress 15235 qusin 15498 catcbas 16040 fpwipodrs 16458 psss 16508 gsumzres 17591 eltg 20020 eltg3 20025 ntrval 20099 restco 20228 restfpw 20243 ordtrest 20266 ordtrest2lem 20267 ordtrest2 20268 cnrmi 20424 restcnrm 20426 kgeni 20600 tsmsfbas 21190 eltsms 21195 tsmsres 21206 caussi 22315 causs 22316 elpwincl1 28202 disjdifprg2 28234 sigainb 29006 ldgenpisyslem1 29033 carsgclctun 29201 eulerpartlemgs2 29261 sseqval 29269 bnj1177 29863 cvmsss2 30045 fnemeet2 31071 ontgval 31139 bj-diagval 31689 fin2so 31976 elrfi 35580 iunrelexp0 36338 fourierdlem71 38078 fourierdlem80 38087 sge0less 38271 sge0ssre 38276 carageniuncllem2 38380 dfrngc2 40246 rnghmsscmap2 40247 rngcbasALTV 40257 dfringc2 40292 rhmsscmap2 40293 rhmsscrnghm 40300 rngcresringcat 40304 ringcbasALTV 40320 srhmsubc 40350 fldc 40357 fldhmsubc 40358 rngcrescrhm 40359 srhmsubcALTV 40369 fldcALTV 40376 fldhmsubcALTV 40377 rngcrescrhmALTV 40378 offval0 40575 |
Copyright terms: Public domain | W3C validator |