Theorem r19.21aiva 1711

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

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

This theorem is referenced by:  rgen2 1720  rgen3 1721  nrexdv 1727  ssrabdv 2122  ss2rabdv 2123  iuneq2dv 2577  iineq2dv 2578  ordunidif 3000  dff2 3808  dffo4 3811  ffnfv 3819  fopabcos 3824  fconst2g 3836  fconstfv 3840  curry1 4088  curry1f 4089  odi 4200  omass 4201  oaabslem 4241  mapenlem2 4476  xpmapenlem4 4485  xpmapenlem5 4486  r1val1 4638  r1val3 4659  ondomcard 4837  lbinfm 6003  flval2t 6189  iccsupr 6339  fsequb2 6464  faclbnd4lem4 6896  sumeq2dv 6938  2sumeq2dv 6940  binomlem1 7012  binomlem2 7013  binomlem4 7015  binomlem5 7016  clm4f 7028  climfnn 7038  climconst3 7041  clim2serz 7089  climserzle 7091  caucvg3t 7112  isum1p 7149  isummulc1ALT 7156  geoisum1c 7188  cvgratlem5 7197  elcncf1d 7213  mulc1cncf 7222  ef0lem 7260  efseq0ex 7261  efaddlem3 7290  efaddlem5 7292  efaddlem6 7293  efaddlem16 7303  efaddlem18 7305  efaddlem19 7306  efaddlem25 7312  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  tgss2t 7587  subtop 7596  idcn 7716  cnco 7718  iscncl 7720  sncld 7737  ismsi 7751  ismeti 7752  opnm 7812  blssopn 7819  metcnp 7839  lmconst 7886  lmfexlem1 7907  metelcls 7916  metcnp4 7920  xplmi 7923  xpcn 7926  oprcn 7927  bopcnlem2 7932  bopcnlem4 7934  bopcn 7935  iscms2 7944  cmsss 7947  bcthlem30 7978  isgrp 7991  grpidinv 8002  grpideu 8003  isgrp2i 8026  grpinvf 8029  isvci 8153  isnvi 8184  invfval 8213  sqcn 8283  nmcnilem 8285  va1cnlem 8292  sm1cnilem 8294  ipcl 8312  ip1cnilem2 8321  ip1cnilem3 8322  ip1cnilem6 8325  sspn 8342  0lno 8395  nmlno0lem 8398  isblo3i 8405  blocnilem 8408  blocni 8409  ipblnfi 8460  ubthlem3 8475  ubthlem4 8476  minveclem9 8497  minveclem29 8517  minveclem30 8518  minveclem31 8519  htthlem11 8573  shftefif1olem 8680  occllem4 9115  occllem6 9117  occl 9120  projlem24 9148  projlem25 9149  projlem26 9150  spansn 9419  hoaddclt 9624  homulclt 9625  homulid2t 9666  homco1t 9667  homulasst 9668  hoadddit 9669  hoadddirt 9670  unoplint 9783  adjvalvalt 9800  hmoplint 9805  brafnt 9810  bralnfnt 9811  kbopt 9816  kbpjt 9819  homco2t 9840  idcnop 9844  nmlnop0ALT 9858  lnophs 9864  lnopeq0 9870  elunop2t 9876  nmopunt 9877  nmophm 9899  lnopcon 9901  lnopcnbdt 9903  lnfncon 9928  lnfncnbdt 9930  nlelch 9932  riesz3 9933  cnlnadjlem2 9939  cnlnadjlem6 9943  adjlnopt 9957  branmfnt 9976  cnvbravalt 9981  kbass2t 9988  leoprf2t 9998  leoprft 9999  leopsqt 10000  leopnmidt 10009  hmopidmpj 10018  pjss1co 10029  pjss2co 10030  pjorthco 10035  pjscj 10036  pjssdif2 10040  pjssdif1 10041  pjinvar 10057  pjclem4 10065  pj3s 10073  mdslmd3 10196  csmdsym 10198  atmd 10263  hmeogrp 10461  homcard 10462  fgsb 10480  fgsb2 10485  efilcp2 10486  t2t1 10496  iint 10514  trdom 10515  cnvtr 10518  idmon 10624

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

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

Copyright terms: Public domain