Theorem r19.21aiva 1714

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

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

This theorem is referenced by:  rgen2 1723  rgen3 1724  nrexdv 1730  ssrabdv 2126  ss2rabdv 2127  iuneq2dv 2582  iineq2dv 2583  ordunidif 3005  dff2 3817  dffo4 3820  ffnfv 3828  fopabcos 3833  fconst2g 3845  fconstfv 3849  curry1 4098  curry1f 4099  odi 4210  omass 4211  oaabslem 4251  mapenlem2 4490  xpmapenlem4 4499  xpmapenlem5 4500  r1val1 4658  r1val3 4679  ondomcard 4857  lbinfm 6048  flval2t 6238  iccsupr 6398  fsequb2 6524  faclbnd4lem4 6951  sumeq2dv 6992  2sumeq2dv 6994  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem5 7070  clm4f 7082  climfnn 7092  climconst3 7096  clim2serz 7145  climserzle 7147  caucvg3t 7168  isum1p 7206  isummulc1ALT 7213  geoisum1c 7245  cvgratlem5 7254  elcncf1d 7270  mulc1cncf 7279  ef0lem 7310  efseq0ex 7311  efaddlem3 7340  efaddlem5 7342  efaddlem6 7343  efaddlem16 7353  efaddlem18 7355  efaddlem19 7356  efaddlem25 7362  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  acdclem 7494  tgss2t 7637  subtop 7646  idcn 7766  cnco 7768  iscncl 7770  sncld 7787  ismsi 7801  ismeti 7802  opnm 7860  blssopn 7867  metcnp 7887  lmconst 7934  lmfexlem1 7956  metelcls 7965  metcnp4 7970  xplmi 7973  xpcn 7976  oprcn 7977  bopcnlem2 7982  bopcnlem4 7984  bopcn 7985  iscms2 7994  cmsss 7997  bcthlem30 8028  isgrp 8041  grpidinv 8052  grpideu 8053  isgrp2i 8076  grpinvf 8079  isvci 8201  isnvi 8232  invfval 8261  sqcn 8335  nmcnilem 8337  va1cnlem 8345  sm1cnilem 8347  ipcl 8365  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem6 8378  sspn 8395  0lno 8450  nmlno0lem 8453  isblo3i 8461  blocnilem 8464  blocni 8465  ipblnfi 8516  ubthlem3 8531  ubthlem4 8532  minveclem9 8553  minveclem29 8573  minveclem30 8574  minveclem31 8575  htthlem11 8630  shftefif1olem 8741  occllem4 9176  occllem6 9178  occl 9181  projlem24 9209  projlem25 9210  projlem26 9211  spansn 9480  hoaddclt 9684  homulclt 9685  homulid2t 9726  homco1t 9727  homulasst 9728  hoadddit 9729  hoadddirt 9730  unoplint 9844  adjvalvalt 9861  hmoplint 9866  brafnt 9871  bralnfnt 9872  kbopt 9877  kbpjt 9880  homco2t 9901  idcnop 9905  nmlnop0ALT 9920  lnophs 9926  lnopeq0 9932  elunop2t 9938  nmopunt 9939  nmophm 9961  lnopcon 9963  lnopcnbdt 9965  lnfncon 9990  lnfncnbdt 9992  nlelch 9994  riesz3 9995  cnlnadjlem2 10001  cnlnadjlem6 10005  adjlnopt 10019  branmfnt 10038  cnvbravalt 10043  kbass2t 10050  leoprf2t 10060  leoprft 10061  leopsqt 10062  leopnmidt 10071  hmopidmpj 10080  pjss1co 10091  pjss2co 10092  pjorthco 10097  pjscj 10098  pjssdif2 10102  pjssdif1 10103  pjinvar 10119  pjclem4 10127  pj3s 10135  mdslmd3 10259  csmdsym 10261  atmd 10326  hmeogrp 10538  homcard 10539  fgsb 10570  fgsbOLD 10571  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  t2t1 10616  iint 10634  trdom 10635  cnvtr 10638  idmon 10745

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975

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

Copyright terms: Public domain