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  4608  rexxfrd  4611  iunpw  4628  fvelima  5757  carden2bex  7541  prnmaddl  7863  prarloclem5  7873  prarloc2  7877  genprndl  7894  genprndu  7895  ltpopr  7968  recexprlemm  7997  recexprlemopl  7998  recexprlemopu  8000  recexprlem1ssl  8006  recexprlem1ssu  8007  cauappcvgprlemupu  8022  caucvgprlemupu  8045  caucvgprprlemupu  8073  caucvgsrlemoffres  8173  map2psrprg  8178  resqrexlemgt0  11808  subcn2  12102  bezoutlembz  12806  pythagtriplem19  13090  mplsubgfileminv  15216  tgcl  15290  neiss  15376  ssnei2  15383  tgcnp  15435  cnptopco  15448  cnptopresti  15464  lmtopcnp  15476  blssexps  15655  blssex  15656  mopni3  15710  neibl  15717  metss  15720  metcnp3  15737  mpomulcn  15792  rescncf  15807  limcresi  15892  plyss  15964  umgrnloop0  16563  uhgr2edg  16652