Theorem r19.21aiva 1706

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)

Hypothesis

Ref	Expression
r19.21aiva.1	|- ((ph /\ x e. A) -> ps)

Assertion

Ref	Expression
r19.21aiva	|- (ph -> A.x e. A ps)

Distinct variable group:   ph,x

Proof of Theorem r19.21aiva

Step	Hyp	Ref	Expression
1		r19.21aiva.1	. . 3 |- ((ph /\ x e. A) -> ps)
2	1	ex 373	. 2 |- (ph -> (x e. A -> ps))
3	2	r19.21aiv 1705	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  A.wral 1637

This theorem is referenced by:  rgen2 1715  rgen3 1716  nrexdv 1722  ssrabdv 2116  ss2rabdv 2117  iuneq2dv 2572  iineq2dv 2573  ordunidif 2995  dff2 3802  dffo4 3805  ffnfv 3813  fopabcos 3818  fconst2g 3830  fconstfv 3834  curry1 4082  curry1f 4083  odi 4194  omass 4195  oaabslem 4235  mapenlem2 4470  xpmapenlem4 4479  xpmapenlem5 4480  r1val1 4630  r1val3 4651  ondomcard 4829  lbinfm 5995  flval2t 6181  iccsupr 6331  fsequb2 6456  faclbnd4lem4 6888  sumeq2dv 6930  2sumeq2dv 6932  binomlem1 7004  binomlem2 7005  binomlem4 7007  binomlem5 7008  clm4f 7020  climfnn 7030  climconst3 7033  clim2serz 7081  climserzle 7083  caucvg3t 7104  isum1p 7141  isummulc1ALT 7148  geoisum1c 7180  cvgratlem5 7189  elcncf1d 7205  mulc1cncf 7214  ef0lem 7252  efseq0ex 7253  efaddlem3 7282  efaddlem5 7284  efaddlem6 7285  efaddlem16 7295  efaddlem18 7297  efaddlem19 7298  efaddlem25 7304  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  tgss2t 7579  subtop 7588  idcn 7705  cnco 7707  iscncl 7709  sncld 7726  ismsi 7740  ismeti 7741  opnm 7800  blssopn 7807  metcnp 7826  lmconst 7872  lmfexlem1 7891  metelcls 7900  metcnp4 7904  xplmi 7907  xpcn 7910  oprcn 7911  bopcnlem2 7916  bopcnlem4 7918  bopcn 7919  iscms2 7928  cmsss 7931  bcthlem30 7962  isgrp 7975  grpidinv 7986  grpideu 7987  isgrp2i 8011  grpinvf 8014  isvci 8139  isnvi 8171  isnviOLD 8172  invfval 8201  sqcn 8270  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  ipcl 8299  ip1cnilem2 8308  ip1cnilem3 8309  ip1cnilem6 8312  sspn 8329  0lno 8382  nmlno0lem 8385  isblo3i 8392  blocnilem 8395  blocni 8396  ipblnfi 8447  ubthlem3 8462  ubthlem4 8463  minveclem9 8484  minveclem29 8504  minveclem30 8505  minveclem31 8506  htthlem11 8560  shftefif1olem 8661  shftefif1olemOLD 8662  occllem4 9092  occllem6 9094  occl 9097  projlem24 9125  projlem25 9126  projlem26 9127  spansn 9396  hoaddclt 9601  homulclt 9602  homulid2t 9643  homco1t 9644  homulasst 9645  hoadddit 9646  hoadddirt 9647  unoplint 9760  adjvalvalt 9777  hmoplint 9782  brafnt 9787  bralnfnt 9788  kbopt 9793  kbpjt 9796  homco2t 9817  idcnop 9821  nmlnop0ALT 9835  lnophs 9841  lnopeq0 9847  elunop2t 9853  nmopunt 9854  nmophm 9876  lnopcon 9878  lnopcnbdt 9880  lnfncon 9905  lnfncnbdt 9907  nlelch 9909  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem6 9920  adjlnopt 9934  branmfnt 9951  cnvbravalt 9956  kbass2t 9962  leoprf2t 9972  leoprft 9973  leopsqt 9974  leopnmidt 9982  hmopidmpj 9991  pjss1co 10002  pjss2co 10003  pjorthco 10008  pjscj 10009  pjssdif2 10013  pjssdif1 10014  pjinvar 10029  pjclem4 10037  pj3s 10045  mdslmd3 10167  csmdsym 10169  atmd 10234  hmeogrp 10425  homcard 10426  fgsb 10444  fgsb2 10449  efilcp2 10450  t2t1 10460  iint 10478  trdom 10479  cnvtr 10482  idmon 10588

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1641

Copyright terms: Public domain