![]() |
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 4062 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∩ 𝐵) = (𝐴 ∩ 𝐵)) | |
2 | 1 | eleq1d 2844 | . 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∩ 𝐵) ∈ V ↔ (𝐴 ∩ 𝐵) ∈ V)) |
3 | vex 3412 | . . 3 ⊢ 𝑥 ∈ V | |
4 | 3 | inex1 5074 | . 2 ⊢ (𝑥 ∩ 𝐵) ∈ V |
5 | 2, 4 | vtoclg 3480 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝐵) ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 Vcvv 3409 ∩ cin 3822 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 ax-sep 5056 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-rab 3091 df-v 3411 df-in 3830 |
This theorem is referenced by: dmresexg 5719 onin 6057 offval 7232 offval3 7493 onsdominel 8460 ssenen 8485 inelfi 8675 fiin 8679 tskwe 9171 dfac8b 9249 ac10ct 9252 infpwfien 9280 fictb 9463 canthnum 9867 gruina 10036 ressinbas 16414 ressress 16416 qusin 16671 catcbas 17227 fpwipodrs 17644 psss 17694 gsumzres 18795 eltg 21281 eltg3 21286 ntrval 21360 restco 21488 restfpw 21503 ordtrest 21526 ordtrest2lem 21527 ordtrest2 21528 cnrmi 21684 restcnrm 21686 kgeni 21861 tsmsfbas 22451 eltsms 22456 tsmsres 22467 caussi 23615 causs 23616 elpwincl1 30072 disjdifprg2 30106 sigainb 31069 ldgenpisyslem1 31096 carsgclctun 31253 eulerpartlemgs2 31312 sseqval 31321 reprinrn 31566 bnj1177 31952 cvmsss2 32135 frrlem13 32685 fnemeet2 33265 ontgval 33328 bj-discrmoore 33943 bj-diagval 33973 fin2so 34349 inex2ALTV 35069 inex3 35070 inxpex 35071 dfrefrels2 35227 dfsymrels2 35255 dftrrels2 35285 elrfi 38715 iunrelexp0 39439 fourierdlem71 41918 fourierdlem80 41927 sge0less 42130 sge0ssre 42135 carageniuncllem2 42260 dfrngc2 43632 rnghmsscmap2 43633 rngcbasALTV 43643 dfringc2 43678 rhmsscmap2 43679 rhmsscrnghm 43686 rngcresringcat 43690 ringcbasALTV 43706 srhmsubc 43736 fldc 43743 fldhmsubc 43744 rngcrescrhm 43745 srhmsubcALTV 43754 fldcALTV 43761 fldhmsubcALTV 43762 rngcrescrhmALTV 43763 offval0 43957 |
Copyright terms: Public domain | W3C validator |