Theorem r19.22dv2 1736

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

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 958  E.wex 980  E.wrex 1646

This theorem is referenced by:  ssrexv 2115  iunss1 2574  mouniss 2890  nnsuc 3148  ssimaex 3768  oaass 4195  oarec 4196  ssnnfi 4535  ssnnfiOLD 4536  zfregs 4647  zorn2lem7 4794  alephval3 4903  neissex 7738  cmsss 7997  shless 9347

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain