Theorem reximdv 2533

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 2532	1 |- ( ph -> ( E. x e. A ps -> E. x e. A ch ) )

Syntax hints:   -> wi 4   e. wcel 1480   E.wrex 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422

This theorem is referenced by:  r19.12  2538  reusv3  4381  rexxfrd  4384  iunpw  4401  fvelima  5473  carden2bex  7045  prnmaddl  7298  prarloclem5  7308  prarloc2  7312  genprndl  7329  genprndu  7330  ltpopr  7403  recexprlemm  7432  recexprlemopl  7433  recexprlemopu  7435  recexprlem1ssl  7441  recexprlem1ssu  7442  cauappcvgprlemupu  7457  caucvgprlemupu  7480  caucvgprprlemupu  7508  caucvgsrlemoffres  7608  map2psrprg  7613  resqrexlemgt0  10792  subcn2  11080  bezoutlembz  11692  tgcl  12233  neiss  12319  ssnei2  12326  tgcnp  12378  cnptopco  12391  cnptopresti  12407  lmtopcnp  12419  blssexps  12598  blssex  12599  mopni3  12653  neibl  12660  metss  12663  metcnp3  12680  rescncf  12737  limcresi  12804