Theorem reximdv2 2914

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)

Hypothesis

Ref	Expression
reximdv2.1	|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )

Assertion

Ref	Expression
reximdv2	|- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem reximdv2

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 |- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ch ) ) )
2	1	eximdv 1697	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2799	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2799	. 2 |- ( E. x e. B ch <-> E. x ( x e. B /\ ch ) )
5	2, 3, 4	3imtr4g 270	1 |- ( ph -> ( E. x e. A ps -> E. x e. B ch ) )

Syntax hints:   -> wi 4   /\ wa 369   E.wex 1599   e. wcel 1804   E.wrex 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

This theorem depends on definitions:  df-bi 185  df-ex 1600  df-rex 2799

This theorem is referenced by:  ssrexv  3550  ssimaex  5923  nnsuc  6702  oaass  7212  omeulem1  7233  ssnnfi  7741  findcard3  7765  unfilem1  7786  epfrs  8165  alephval3  8494  isfin7-2  8779  fin1a2lem6  8788  fpwwe2lem12  9022  fpwwe2lem13  9023  inawinalem  9070  ico0  11584  ioc0  11585  r19.2uz  13163  climrlim2  13349  iserodd  14236  ramub2  14409  pgpssslw  16508  efgrelexlemb  16642  ablfaclem3  17012  unitgrp  17190  lspsneq  17642  lbsextlem4  17681  neissex  19501  iscnp4  19637  nlly2i  19850  llynlly  19851  restnlly  19856  llyrest  19859  nllyrest  19860  llyidm  19862  nllyidm  19863  qtophmeo  20191  cnpflfi  20373  cnextcn  20440  ivthlem3  21738  ovolicc2lem5  21805  dvfsumrlim  22305  itgsubst  22323  lgsquadlem2  23502  footex  23967  opphllem1  23991  nbgraf1olem5  24317  cusgrafilem2  24352  cmppcmp  27734  eulerpartlemgvv  28188  eulerpartlemgh  28190  erdszelem7  28514  rellyscon  28569  trpredrec  29296  itg2gt0cn  30045  ivthALT  30128  fnessref  30150  frinfm  30201  sstotbnd2  30245  heiborlem3  30284  isdrngo3  30337  pellexlem5  30744  pell14qrss1234  30767  pell1qrss14  30779  pellfundglb  30796  lnr2i  31040  hbtlem6  31053  dihjat1lem  36895  dvh1dim  36909  dochsatshp  36918  lcfl6  36967  mapdval2N  37097  mapdpglem2  37140  hdmaprnlem10N  37329