Theorem inex1g 4559

Description: Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.)

Assertion

Ref	Expression
inex1g	|- ( A e. V -> ( A i^i B ) e. _V )

Proof of Theorem inex1g

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ineq1 3638	. . 3 |- ( x = A -> ( x i^i B ) = ( A i^i B ) )
2	1	eleq1d 2523	. 2 |- ( x = A -> ( ( x i^i B ) e. _V <-> ( A i^i B ) e. _V ) )
3		vex 3059	. . 3 |- x e. _V
4	3	inex1 4557	. 2 |- ( x i^i B ) e. _V
5	2, 4	vtoclg 3118	1 |- ( A e. V -> ( A i^i B ) e. _V )

Syntax hints:   -> wi 4   = wceq 1454   e. wcel 1897   _Vcvv 3056   i^i cin 3414

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