Theorem r19.41v 3089

Description: Restricted quantifier version 19.41v 1914. Version of r19.41 3090 with a dv condition, requiring fewer axioms. (Contributed by NM, 17-Dec-2003.) Reduce dependencies on axioms. (Revised by BJ, 29-Mar-2020.)

Assertion

Ref	Expression
r19.41v	|- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )

Distinct variable group:   ps, x

Allowed substitution hints:   ph( x)   A( x)

Proof of Theorem r19.41v

Step	Hyp	Ref	Expression
1		anass 681	. . . 4 |- ( ( ( x e. A /\ ph ) /\ ps ) <-> ( x e. A /\ ( ph /\ ps ) ) )
2	1	exbii 1774	. . 3 |- ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
3		19.41v 1914	. . 3 |- ( E. x ( ( x e. A /\ ph ) /\ ps ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
4	2, 3	bitr3i 266	. 2 |- ( E. x ( x e. A /\ ( ph /\ ps ) ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
5		df-rex 2918	. 2 |- ( E. x e. A ( ph /\ ps ) <-> E. x ( x e. A /\ ( ph /\ ps ) ) )
6		df-rex 2918	. . 3 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
7	6	anbi1i 731	. 2 |- ( ( E. x e. A ph /\ ps ) <-> ( E. x ( x e. A /\ ph ) /\ ps ) )
8	4, 5, 7	3bitr4i 292	1 |- ( E. x e. A ( ph /\ ps ) <-> ( E. x e. A ph /\ ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704   e. wcel 1990   E.wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  r19.41vv  3091  r19.42v  3092  3reeanv  3108  reuind  3411  iuncom4  4528  dfiun2g  4552  iunxiun  4608  inuni  4826  reuxfrd  4893  xpiundi  5173  xpiundir  5174  imaco  5640  coiun  5645  abrexco  6502  imaiun  6503  isomin  6587  isoini  6588  oarec  7642  mapsnen  8035  genpass  9831  4fvwrd4  12459  4sqlem12  15660  imasleval  16201  lsmspsn  19084  utoptop  22038  metrest  22329  metust  22363  cfilucfil  22364  metuel2  22370  istrkg2ld  25359  axsegcon  25807  fusgreg2wsp  27200  nmoo0  27646  hhcmpl  28057  nmop0  28845  nmfn0  28846  reuxfr4d  29330  rexunirn  29331  ordtconnlem1  29970  dya2icoseg2  30340  dya2iocnei  30344  omssubaddlem  30361  omssubadd  30362  bj-mpt2mptALT  33072  mptsnunlem  33185  rabiun  33382  iundif1  33383  poimir  33442  ismblfin  33450  prtlem11  34151  prter2  34166  prter3  34167  islshpat  34304  lshpsmreu  34396  islpln5  34821  islvol5  34865  cdlemftr3  35853  dvhb1dimN  36274  dib1dim  36454  mapdpglem3  36964  hdmapglem7a  37219  diophrex  37339  mapsnend  39391