![]() |
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 4202 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵)) | |
2 | 1 | eleq1d 2814 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V)) |
3 | vex 3474 | . . 3 ⊢ 𝑥 ∈ V | |
4 | 3 | inex1 5312 | . 2 ⊢ (𝑥 ∩ 𝐵) ∈ V |
5 | 2, 4 | vtoclg 3539 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1534 ∈ wcel 2099 Vcvv 3470 ∩ cin 3944 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5294 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-rab 3429 df-v 3472 df-in 3952 |
This theorem is referenced by: inex2g 5315 dmresexg 6004 predexg 6318 onin 6395 offval 7689 offval3 7981 frrlem13 8298 onsdominel 9145 ssenen 9170 inelfi 9436 fiin 9440 tskwe 9968 dfac8b 10049 ac10ct 10052 infpwfien 10080 fictb 10263 canthnum 10667 gruina 10836 ressinbas 17220 ressress 17223 qusin 17520 catcbas 18084 fpwipodrs 18526 psss 18566 gsumzres 19858 dfrngc2 20555 rnghmsscmap2 20556 dfringc2 20584 rhmsscmap2 20585 rhmsscrnghm 20592 rngcresringcat 20596 srhmsubc 20607 rngcrescrhm 20611 fldc 20666 fldhmsubc 20667 eltg 22854 eltg3 22859 ntrval 22934 restco 23062 restfpw 23077 ordtrest 23100 ordtrest2lem 23101 ordtrest2 23102 cnrmi 23258 restcnrm 23260 kgeni 23435 tsmsfbas 24026 eltsms 24031 tsmsres 24042 caussi 25219 causs 25220 elpwincl1 32316 disjdifprg2 32360 sigainb 33750 ldgenpisyslem1 33777 carsgclctun 33936 eulerpartlemgs2 33995 sseqval 34003 reprinrn 34245 bnj1177 34632 cvmsss2 34879 satef 35021 satefvfmla0 35023 fnemeet2 35846 ontgval 35910 bj-discrmoore 36585 bj-ideqb 36633 bj-opelidres 36635 bj-opelidb1ALT 36640 fin2so 37075 inex3 37805 inxpex 37806 dfrefrels2 37980 dfsymrels2 38012 dftrrels2 38042 elrfi 42105 ofoafg 42774 fourierdlem71 45556 fourierdlem80 45565 sge0less 45771 sge0ssre 45776 carageniuncllem2 45901 rngcbasALTV 47319 rngcrescrhmALTV 47333 ringcbasALTV 47353 srhmsubcALTV 47378 fldcALTV 47385 fldhmsubcALTV 47386 |
Copyright terms: Public domain | W3C validator |