Theorem reximdv2 2820

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 1676	. 2 |- ( ph -> ( E. x ( x e. A /\ ps ) -> E. x ( x e. B /\ ch ) ) )
3		df-rex 2716	. 2 |- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
4		df-rex 2716	. 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 1586   e. wcel 1756   E.wrex 2711

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

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-rex 2716

This theorem is referenced by:  ssrexv  3412  ssimaex  5751  nnsuc  6488  oaass  6992  omeulem1  7013  ssnnfi  7524  findcard3  7547  unfilem1  7568  epfrs  7943  alephval3  8272  isfin7-2  8557  fin1a2lem6  8566  fpwwe2lem12  8800  fpwwe2lem13  8801  inawinalem  8848  ico0  11338  ioc0  11339  r19.2uz  12831  climrlim2  13017  iserodd  13894  ramub2  14067  pgpssslw  16104  efgrelexlemb  16238  ablfaclem3  16578  unitgrp  16749  lspsneq  17183  lbsextlem4  17222  neissex  18711  iscnp4  18847  nlly2i  19060  llynlly  19061  restnlly  19066  llyrest  19069  nllyrest  19070  llyidm  19072  nllyidm  19073  qtophmeo  19370  cnpflfi  19552  cnextcn  19619  ivthlem3  20917  ovolicc2lem5  20984  dvfsumrlim  21483  itgsubst  21501  lgsquadlem2  22674  nbgraf1olem5  23322  cusgrafilem2  23356  eulerpartlemgvv  26728  eulerpartlemgh  26730  erdszelem7  27054  rellyscon  27109  trpredrec  27671  itg2gt0cn  28418  ivthALT  28501  fnessref  28536  frinfm  28600  sstotbnd2  28644  heiborlem3  28683  isdrngo3  28736  pellexlem5  29145  pell14qrss1234  29168  pell1qrss14  29180  pellfundglb  29197  lnr2i  29443  hbtlem6  29456  dihjat1lem  34966  dvh1dim  34980  dochsatshp  34989  lcfl6  35038  mapdval2N  35168  mapdpglem2  35211  hdmaprnlem10N  35400