Theorem r19.23aiv 1743

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 971	. 2 |- (ps -> A.xps)
2		r19.23aiv.1	. 2 |- (x e. A -> (ph -> ps))
3	1, 2	r19.23ai 1742	1 |- (E.x e. A ph -> ps)

Syntax hints:   -> wi 3   e. wcel 958  E.wrex 1646

This theorem is referenced by:  r19.23aiva 1744  r19.23aivv 1748  r19.36av 1760  r19.44av 1766  r19.45av 1767  rexn0 2356  uniss2 2529  eliun 2570  frirr 2924  fr2nr 2925  fr3nr 2926  onuninsuc 3108  ordzsl 3116  onzsl 3117  fvelrnb 3760  fvelimab 3765  ssimaex 3768  tfrlem4 3914  abianfp 3962  oprvalelrn 4039  mapsn 4345  isfi 4382  php 4513  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  domfiOLD 4539  unifiOLD 4557  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  fodomfibOLD 4567  iunfiOLD 4569  pwfiOLD 4571  inf0 4606  inf3lemd 4612  inf3lem6 4618  trcl 4645  rankr1 4674  bndrank 4682  rankc2 4706  rankxpsuc 4715  scott0 4717  aceq5lem4 4738  aceq6b 4742  ac6lem 4754  weth 4787  zorn2lem7 4794  cardiun 4859  cardalephex 4886  isinfcard 4887  alephfp 4900  cnegextlem2 5346  negeu 5355  receu 5701  infmrcl 6069  bndndx 6073  elq 6257  om2uzran 6300  limsupclt 6530  sqrlem20 6692  cau5i 6917  cvg1 6921  cvg3 6923  caubnd 6926  climshft 7104  caucvglem2 7158  caucvg3lem 7166  cvgcmpub 7185  infcvgaux1 7219  ruclem33 7542  ruclem35 7544  infxpidmlem12 7563  retopbas 7655  ntrss2 7690  ssnei 7724  opnneiid 7737  sncld 7787  caun0 7945  minveclem10 8554  circgrp 8740  projlem8 9193  projlem15 9200  pjth 9233  h1de2ctlem 9478  h1de2ct 9479  spansn 9480  spanunsn 9502  nmcopexlem6 9956  nmcfnexlem6 9985  riesz3 9995  adjbd1o 10018  rnbra 10040  pjnmop 10075  atom1d 10280  cvexchlem 10295  cdj1 10360  cdj3lem1 10361  ghomgrpilem2 10386  homcard 10539  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain