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  11786  subcn2  12077  bezoutlembz  12781  pythagtriplem19  13061  mplsubgfileminv  15091  tgcl  15165  neiss  15251  ssnei2  15258  tgcnp  15310  cnptopco  15323  cnptopresti  15339  lmtopcnp  15351  blssexps  15530  blssex  15531  mopni3  15585  neibl  15592  metss  15595  metcnp3  15612  mpomulcn  15667  rescncf  15682  limcresi  15767  plyss  15839  umgrnloop0  16358  uhgr2edg  16447