Theorem inex1g 4534

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 3631	. . 3 |- ( x = A -> ( x i^i B ) = ( A i^i B ) )
2	1	eleq1d 2469	. 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 4532	. 2 |- ( x i^i B ) e. _V
5	2, 4	vtoclg 3114	1 |- ( A e. V -> ( A i^i B ) e. _V )

Syntax hints:   -> wi 4   = wceq 1403   e. wcel 1840   _Vcvv 3056   i^i cin 3410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-v 3058  df-in 3418

This theorem is referenced by:  onin  4850  dmresexg  5235  offval  6482  offval3  6730  onsdominel  7622  ssenen  7647  inelfi  7830  fiin  7834  tskwe  8281  dfac8b  8362  ac10ct  8365  infpwfien  8393  fictb  8575  canthnum  8975  gruina  9144  ressinbas  14794  ressress  14796  qusin  15048  catcbas  15590  fpwipodrs  16008  psss  16058  gsumzres  17128  gsumzresOLD  17132  eltg  19640  eltg3  19645  ntrval  19719  restco  19848  restfpw  19863  ordtrest  19886  ordtrest2lem  19887  ordtrest2  19888  cnrmi  20044  restcnrm  20046  kgeni  20220  tsmsfbas  20808  eltsms  20813  tsmsresOLD  20827  tsmsres  20828  caussi  21918  causs  21919  elpwincl1  27716  disjdifprg2  27749  sigainb  28465  ldgenpisyslem1  28492  carsgclctun  28650  eulerpartlemgs2  28706  sseqval  28714  bnj1177  29265  cvmsss2  29447  epsetlike  29942  fnemeet2  30578  ontgval  30646  bj-diagval  31153  fin2so  31376  elrfi  34952  iunrelexp0  35645  fourierdlem71  37295  fourierdlem80  37304  dfrngc2  38224  rnghmsscmap2  38225  rngcbasALTV  38235  dfringc2  38270  rhmsscmap2  38271  rhmsscrnghm  38278  rngcresringcat  38282  ringcbasALTV  38298  srhmsubc  38328  fldc  38335  fldhmsubc  38336  rngcrescrhm  38337  srhmsubcALTV  38347  fldcALTV  38354  fldhmsubcALTV  38355  rngcrescrhmALTV  38356  offval0  38555