Theorem r19.23aiv 1735

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

Hypothesis

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

Assertion

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

Distinct variable group:   ps,x

Proof of Theorem r19.23aiv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ps -> A.xps)
2		r19.23aiv.1	. 2 |- (x e. A -> (ph -> ps))
3	1, 2	r19.23ai 1734	1 |- (E.x e. A ph -> ps)

Syntax hints:   -> wi 3   e. wcel 955  E.wrex 1638

This theorem is referenced by:  r19.23aiva 1736  r19.23aivv 1740  r19.36av 1752  r19.44av 1758  r19.45av 1759  rexn0 2346  uniss2 2519  eliun 2560  frirr 2914  fr2nr 2915  fr3nr 2916  onuninsuc 3098  ordzsl 3106  onzsl 3107  fvelrnb 3745  fvelimab 3750  ssimaex 3753  tfrlem4 3899  abianfp 3947  oprvalelrn 4024  mapsn 4329  php 4493  php3 4495  ssfi 4515  domfi 4516  unifi 4532  fiint 4534  fodomfi 4540  fodomfib 4541  iunfi 4543  pwfi 4545  inf0 4578  inf3lemd 4584  inf3lem6 4590  trcl 4617  rankr1 4646  bndrank 4654  rankc2 4678  rankxpsuc 4687  scott0 4689  aceq5lem4 4710  aceq6b 4714  ac6lem 4726  weth 4759  zorn2lem7 4766  cardiun 4831  cardalephex 4858  isinfcard 4859  alephfp 4872  cnegextlem2 5318  negeu 5327  receu 5670  infmrcl 6016  bndndx 6020  elq 6195  om2uzran 6237  limsupclt 6462  sqrlem20 6622  cau5i 6854  cvg1 6858  cvg3 6860  caubnd 6863  climshft 7041  caucvglem2 7094  caucvg3lem 7102  cvgcmpub 7121  infcvgaux1 7154  ruclem33 7485  ruclem35 7487  infxpidmlem12 7506  retopbas 7597  ntrss2 7632  ssnei 7665  opnneiid 7678  sncld 7726  caun0 7880  minveclem10 8485  circgrp 8660  projlem8 9109  projlem15 9116  pjth 9148  h1de2ctlem 9394  h1de2ct 9395  spansn 9396  spanunsn 9419  nmcopexlem6 9871  nmcfnexlem6 9900  riesz3 9910  adjbd1o 9933  rnbra 9953  pjnmop 9986  atom1d 10188  cvexchlem 10203  cdj1 10265  cdj3lem1 10266  ghomgrpilem2 10291  homcard 10426  fgsb 10444  efilcp 10445  fgsb2 10449  efilcp2 10450

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  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain