Theorem reximdv 2651

Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)

Hypothesis

Ref	Expression
reximdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

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

Distinct variable group:   ph, x

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

Proof of Theorem reximdv

Step	Hyp	Ref	Expression
1		reximdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 22	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	reximdvai 2650	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  r19.12  2657  reusv3  4606  rexxfrd  4609  iunpw  4626  fvelima  5754  carden2bex  7535  prnmaddl  7857  prarloclem5  7867  prarloc2  7871  genprndl  7888  genprndu  7889  ltpopr  7962  recexprlemm  7991  recexprlemopl  7992  recexprlemopu  7994  recexprlem1ssl  8000  recexprlem1ssu  8001  cauappcvgprlemupu  8016  caucvgprlemupu  8039  caucvgprprlemupu  8067  caucvgsrlemoffres  8167  map2psrprg  8172  resqrexlemgt0  11800  subcn2  12093  bezoutlembz  12797  pythagtriplem19  13081  mplsubgfileminv  15140  tgcl  15214  neiss  15300  ssnei2  15307  tgcnp  15359  cnptopco  15372  cnptopresti  15388  lmtopcnp  15400  blssexps  15579  blssex  15580  mopni3  15634  neibl  15641  metss  15644  metcnp3  15661  mpomulcn  15716  rescncf  15731  limcresi  15816  plyss  15888  umgrnloop0  16456  uhgr2edg  16545