Theorem r19.21aiv 1710

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 969	. 2 |- (ph -> A.xph)
2		r19.21aiv.1	. 2 |- (ph -> (x e. A -> ps))
3	1, 2	r19.21ai 1709	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 956  A.wral 1642

This theorem is referenced by:  r19.21aiva 1711  r19.21aivv 1717  r19.37av 1758  rzal 2351  trin 2685  class2seteq 2730  ralxfr 2894  ssorduni 2988  onmindif 3055  onmindif2 3056  suceloni 3057  limuni3 3118  ralxp 3213  dmxp 3327  dffun7 3532  eqfnfv 3788  ffnfv 3819  abrexex 3851  isocnv 3887  isotr 3888  f1oiso 3895  tfrlem12 3913  tz7.48-2 3948  oaass 4185  omass 4201  oelim2 4212  omsmo 4247  en2d 4387  dom2d 4391  pw2en 4432  mapenlem2 4476  unblem4 4526  unbnn2 4528  iunfi 4549  supmaxlem 4568  suppr 4570  supsnALT 4572  elirrv 4578  trcl 4625  r1tr 4634  tz9.13 4643  scottex 4696  scott0 4697  aceq3 4713  aceq5lem5 4719  ac6lem 4734  kmlem4 4748  kmlem11 4755  numthlem 4763  uniimadom 4790  ondomon 4836  cardmin 4840  carduniima 4870  alephval2 4882  alephval3 4883  cfsuc 4895  genpcl 5091  ltexprlem5 5126  suplem1pr 5141  negeu 5335  receu 5678  lbinfm 6003  xrsupsslem 6031  xrinfmsslem 6032  supxrun 6040  supxrpnf 6043  supxrunb1 6044  supxrunb2 6045  uzind 6161  uzwo4OLD 6166  uzwo3lem1 6172  uzwo3lem2 6173  flval3t 6190  seq1rn2 6266  uzwo 6395  uzwoOLD 6396  fsequb 6463  seqzeq 6495  seqzrn2 6496  recant 6850  cvg2 6867  fsum1 6951  fsumconst 6984  serzcl2t 6995  climconst2 7040  2climnn 7047  2climnn0 7048  iserzshft2 7052  climaddlem3 7060  climmullem8 7071  clim2serzt 7078  iserzmulc1 7080  iserzcmp 7086  climabslem 7092  climubi 7097  climsup 7099  climcau 7100  caucvg 7107  serzf0 7113  ser1f0 7114  ser1clim0 7117  isumreclt 7153  reccnv 7161  expcnv 7176  cvgratlem5 7197  fsum0diag2 7202  fsum0diag4 7204  reeftlclt 7330  effsumle 7346  efcn 7371  unbenlem 7455  infxpidmlem7 7509  unctb 7527  tgclt 7574  bastop 7592  subbas 7594  distop 7599  neif 7665  unnei 7685  cnpco 7719  cncnplem4 7727  cnconst 7730  bl2in 7795  metcnp 7839  tgioo 7867  lmconst 7886  lmuni 7902  lmfexlem3 7909  metelcls 7916  xplm 7925  lmcau 7946  bcthlem22 7970  bcthlem28 7976  grplactf1o 8049  nmoubi 8380  nmobndi 8383  blocni 8409  ip2eqi 8461  ubthlem13 8485  ubthlem14 8486  hial2eqt 8911  hlim0 9044  ocsh 9095  occont 9099  projlem26 9150  projlem29 9153  projlem31 9155  pjthlem14 9170  pjtheu 9173  shintcl 9231  hsupss 9247  spanss 9256  osumlem5 9522  nmopubt 9772  nmfnleubt 9788  nmcopexlem6 9894  nmcfnexlem6 9923  pjnmop 10013  pjss2co 10030  pjnormss 10034  pjclem4 10065  pj3s 10073  pj3cor1 10075  strlem3a 10117  strb 10123  hstrlem3a 10125  hstrb 10131  spansncv2t 10158  ssmd1 10175  mdsl1 10185  cvmd 10188  mdexch 10199  h1dat 10213  chrelat2 10229  mdsymlem6 10272  sumdmdi 10278  dmdbr5at 10284  cayleylem2 10344  mapdiscn 10434  mapudiscn 10435  hmeogrp 10461  qusp 10466  hgrablkne0 10645  hgrablkcard 10646

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

Copyright terms: Public domain