Theorem r19.22dv2 1739

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.22dv2

Step	Hyp	Ref	Expression
1		r19.22dv2.1	. . 3 |- (ph -> ((x e. A /\ ps) -> (x e. B /\ ch)))
2	1	19.22dv 1292	. 2 |- (ph -> (E.x(x e. A /\ ps) -> E.x(x e. B /\ ch)))
3		df-rex 1653	. 2 |- (E.x e. A ps <-> E.x(x e. A /\ ps))
4		df-rex 1653	. 2 |- (E.x e. B ch <-> E.x(x e. B /\ ch))
5	2, 3, 4	3imtr4g 555	1 |- (ph -> (E.x e. A ps -> E.x e. B ch))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 960  E.wex 982  E.wrex 1649

This theorem is referenced by:  ssrexv 2118  iunss1 2578  mouniss 2896  nnsuc 3154  ssimaex 3774  oaass 4201  oarec 4202  ssnnfi 4545  ssnnfiOLD 4546  zfregs 4657  zorn2lem7 4804  alephval3 4914  neissex 7735  cmsss 7994  shless 9342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain