Theorem inex1g 4801

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 3807	. . 3 |- ( x = A -> ( x i^i B ) = ( A i^i B ) )
2	1	eleq1d 2686	. 2 |- ( x = A -> ( ( x i^i B ) e. _V <-> ( A i^i B ) e. _V ) )
3		vex 3203	. . 3 |- x e. _V
4	3	inex1 4799	. 2 |- ( x i^i B ) e. _V
5	2, 4	vtoclg 3266	1 |- ( A e. V -> ( A i^i B ) e. _V )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  dmresexg  5421  onin  5754  offval  6904  offval3  7162  onsdominel  8109  ssenen  8134  inelfi  8324  fiin  8328  tskwe  8776  dfac8b  8854  ac10ct  8857  infpwfien  8885  fictb  9067  canthnum  9471  gruina  9640  ressinbas  15936  ressress  15938  qusin  16204  catcbas  16747  fpwipodrs  17164  psss  17214  gsumzres  18310  eltg  20761  eltg3  20766  ntrval  20840  restco  20968  restfpw  20983  ordtrest  21006  ordtrest2lem  21007  ordtrest2  21008  cnrmi  21164  restcnrm  21166  kgeni  21340  tsmsfbas  21931  eltsms  21936  tsmsres  21947  caussi  23095  causs  23096  elpwincl1  29357  disjdifprg2  29389  sigainb  30199  ldgenpisyslem1  30226  carsgclctun  30383  eulerpartlemgs2  30442  sseqval  30450  reprinrn  30696  bnj1177  31074  cvmsss2  31256  fnemeet2  32362  ontgval  32430  bj-discrmoore  33066  bj-diagval  33090  fin2so  33396  inex2ALTV  34105  inex3  34106  inxpex  34107  elrfi  37257  iunrelexp0  37994  fourierdlem71  40394  fourierdlem80  40403  sge0less  40609  sge0ssre  40614  carageniuncllem2  40736  dfrngc2  41972  rnghmsscmap2  41973  rngcbasALTV  41983  dfringc2  42018  rhmsscmap2  42019  rhmsscrnghm  42026  rngcresringcat  42030  ringcbasALTV  42046  srhmsubc  42076  fldc  42083  fldhmsubc  42084  rngcrescrhm  42085  srhmsubcALTV  42094  fldcALTV  42101  fldhmsubcALTV  42102  rngcrescrhmALTV  42103  offval0  42299