Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > inex1g | Structured version Visualization version GIF version |
Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |
Ref | Expression |
---|---|
inex1g | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1 4180 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵)) | |
2 | 1 | eleq1d 2897 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V)) |
3 | vex 3498 | . . 3 ⊢ 𝑥 ∈ V | |
4 | 3 | inex1 5213 | . 2 ⊢ (𝑥 ∩ 𝐵) ∈ V |
5 | 2, 4 | vtoclg 3568 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 Vcvv 3495 ∩ cin 3934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3497 df-in 3942 |
This theorem is referenced by: inex2g 5216 dmresexg 5871 onin 6216 offval 7405 offval3 7674 onsdominel 8655 ssenen 8680 inelfi 8871 fiin 8875 tskwe 9368 dfac8b 9446 ac10ct 9449 infpwfien 9477 fictb 9656 canthnum 10060 gruina 10229 ressinbas 16550 ressress 16552 qusin 16807 catcbas 17347 fpwipodrs 17764 psss 17814 gsumzres 18960 eltg 21495 eltg3 21500 ntrval 21574 restco 21702 restfpw 21717 ordtrest 21740 ordtrest2lem 21741 ordtrest2 21742 cnrmi 21898 restcnrm 21900 kgeni 22075 tsmsfbas 22665 eltsms 22670 tsmsres 22681 caussi 23829 causs 23830 elpwincl1 30214 disjdifprg2 30255 sigainb 31295 ldgenpisyslem1 31322 carsgclctun 31479 eulerpartlemgs2 31538 sseqval 31546 reprinrn 31789 bnj1177 32176 cvmsss2 32419 satef 32561 satefvfmla0 32563 frrlem13 33033 fnemeet2 33613 ontgval 33677 bj-discrmoore 34298 bj-ideqb 34344 bj-opelidres 34346 bj-opelidb1ALT 34351 fin2so 34761 inex3 35478 inxpex 35479 dfrefrels2 35635 dfsymrels2 35663 dftrrels2 35693 elrfi 39171 iunrelexp0 39927 fourierdlem71 42343 fourierdlem80 42352 sge0less 42555 sge0ssre 42560 carageniuncllem2 42685 dfrngc2 44141 rnghmsscmap2 44142 rngcbasALTV 44152 dfringc2 44187 rhmsscmap2 44188 rhmsscrnghm 44195 rngcresringcat 44199 ringcbasALTV 44215 srhmsubc 44245 fldc 44252 fldhmsubc 44253 rngcrescrhm 44254 srhmsubcALTV 44263 fldcALTV 44270 fldhmsubcALTV 44271 rngcrescrhmALTV 44272 |
Copyright terms: Public domain | W3C validator |