Theorem r19.22dv2 1743

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 1296	. 2 |- (ph -> (E.x(x e. A /\ ps) -> E.x(x e. B /\ ch)))
3		df-rex 1657	. 2 |- (E.x e. A ps <-> E.x(x e. A /\ ps))
4		df-rex 1657	. 2 |- (E.x e. B ch <-> E.x(x e. B /\ ch))
5	2, 3, 4	3imtr4g 556	1 |- (ph -> (E.x e. A ps -> E.x e. B ch))

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 962  E.wex 984  E.wrex 1653

This theorem is referenced by:  ssrexv 2124  iunss1 2586  mouniss 2904  nnsuc 3162  ssimaex 3782  oaass 4209  oarec 4210  ssnnfi 4550  zfregs 4659  zorn2lem7 4806  alephval3 4916  neissex 7747  cmsss 8006  shless 9354

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 985  df-rex 1657

Copyright terms: Public domain