Theorem inex1g 4430

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 3540	. . 3 |- ( x = A -> ( x i^i B ) = ( A i^i B ) )
2	1	eleq1d 2504	. 2 |- ( x = A -> ( ( x i^i B ) e. _V <-> ( A i^i B ) e. _V ) )
3		vex 2970	. . 3 |- x e. _V
4	3	inex1 4428	. 2 |- ( x i^i B ) e. _V
5	2, 4	vtoclg 3025	1 |- ( A e. V -> ( A i^i B ) e. _V )

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756   _Vcvv 2967   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330

This theorem is referenced by:  onin  4745  dmresexg  5128  offval  6322  offval3  6566  onsdominel  7452  ssenen  7477  inelfi  7660  fiin  7664  tskwe  8112  dfac8b  8193  ac10ct  8196  infpwfien  8224  fictb  8406  canthnum  8808  gruina  8977  ressinbas  14226  ressress  14227  divsin  14474  catcbas  14957  fpwipodrs  15326  psss  15376  gsumzres  16379  gsumzresOLD  16383  eltg  18537  eltg3  18542  ntrval  18615  restco  18743  restfpw  18758  ordtrest  18781  ordtrest2lem  18782  ordtrest2  18783  cnrmi  18939  restcnrm  18941  kgeni  19085  tsmsfbas  19673  eltsms  19678  tsmsresOLD  19692  tsmsres  19693  caussi  20783  causs  20784  disjdifprg2  25871  sigainb  26531  eulerpartlemgs2  26715  sseqval  26723  cvmsss2  27115  epsetlike  27606  ontgval  28229  fin2so  28369  fnemeet2  28541  elrfi  28983  bnj1177  31884  bj-diagval  32372