Theorem r19.21aiv 1705

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

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.21aiv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.xph)
2		r19.21aiv.1	. 2 |- (ph -> (x e. A -> ps))
3	1, 2	r19.21ai 1704	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 955  A.wral 1637

This theorem is referenced by:  r19.21aiva 1706  r19.21aivv 1712  r19.37av 1753  rzal 2345  trin 2680  class2seteq 2725  ralxfr 2889  ssorduni 2983  onmindif 3050  onmindif2 3051  suceloni 3052  limuni3 3113  ralxp 3208  dmxp 3321  dffun7 3526  eqfnfv 3782  ffnfv 3813  abrexex 3845  isocnv 3881  isotr 3882  f1oiso 3889  tfrlem12 3907  tz7.48-2 3942  oaass 4179  omass 4195  oelim2 4206  omsmo 4241  en2d 4381  dom2d 4385  pw2en 4426  mapenlem2 4470  unblem4 4520  unbnn2 4522  iunfi 4543  suppr 4562  supsnALT 4564  elirrv 4570  trcl 4617  r1tr 4626  tz9.13 4635  scottex 4688  scott0 4689  aceq3 4705  aceq5lem5 4711  ac6lem 4726  kmlem4 4740  kmlem11 4747  numthlem 4755  uniimadom 4782  ondomon 4828  cardmin 4832  carduniima 4862  alephval2 4874  alephval3 4875  cfsuc 4887  genpcl 5083  ltexprlem5 5118  suplem1pr 5133  negeu 5327  receu 5670  lbinfm 5995  xrsupsslem 6023  xrinfmsslem 6024  supxrun 6032  supxrpnf 6035  supxrunb1 6036  supxrunb2 6037  uzind 6153  uzwo4OLD 6158  uzwo3lem1 6164  uzwo3lem2 6165  flval3t 6182  seq1rn2 6258  uzwo 6387  uzwoOLD 6388  fsequb 6455  seqzeq 6487  seqzrn2 6488  recant 6842  cvg2 6859  fsum1 6943  fsumconst 6976  serzcl2t 6987  climconst2 7032  2climnn 7039  2climnn0 7040  iserzshft2 7044  climaddlem3 7052  climmullem8 7063  clim2serzt 7070  iserzmulc1 7072  iserzcmp 7078  climabslem 7084  climubi 7089  climsup 7091  climcau 7092  caucvg 7099  serzf0 7105  ser1f0 7106  ser1clim0 7109  isumreclt 7145  reccnv 7153  expcnv 7168  cvgratlem5 7189  fsum0diag2 7194  fsum0diag4 7196  reeftlclt 7322  effsumle 7338  efcn 7363  unbenlem 7447  infxpidmlem7 7501  unctb 7519  tgclt 7566  bastop 7584  subbas 7586  distop 7591  neif 7656  unnei 7676  cnpco 7708  cncnplem4 7716  cnconst 7719  bl2in 7783  metcnp 7826  tgioo 7854  lmconst 7872  lmuni 7886  lmfexlem3 7893  metelcls 7900  xplm 7909  lmcau 7930  bcthlem22 7954  bcthlem28 7960  grplactf1o 8034  nmoubi 8367  nmobndi 8370  blocni 8396  ip2eqi 8448  ubthlem13 8472  ubthlem14 8473  hial2eqt 8893  hlim0 9026  ocsh 9072  occont 9076  projlem26 9127  projlem29 9130  projlem31 9132  pjthlem14 9147  pjtheu 9150  shintcl 9208  hsupss 9224  spanss 9233  osumlem5 9499  nmopubt 9749  nmfnleubt 9765  nmcopexlem6 9871  nmcfnexlem6 9900  pjnmop 9986  pjss2co 10003  pjnormss 10007  pjclem4 10037  pj3s 10045  pj3cor1 10047  strlem3a 10089  strb 10095  hstrlem3a 10097  hstrb 10103  spansncv2t 10130  ssmd1 10146  mdsl1 10156  cvmd 10159  mdexch 10170  h1dat 10184  chrelat2 10200  mdsymlem6 10243  sumdmdi 10249  dmdbr5at 10255  cayleylem2 10317  mapdiscn 10398  mapudiscn 10399  hmeogrp 10425  qusp 10430  hgrablkne0 10609  hgrablkcard 10610

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-ral 1641

Copyright terms: Public domain