Theorem r19.23aiv 1740

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

Syntax hints:   -> wi 3   e. wcel 956  E.wrex 1643

This theorem is referenced by:  r19.23aiva 1741  r19.23aivv 1745  r19.36av 1757  r19.44av 1763  r19.45av 1764  rexn0 2352  uniss2 2524  eliun 2565  frirr 2919  fr2nr 2920  fr3nr 2921  onuninsuc 3103  ordzsl 3111  onzsl 3112  fvelrnb 3751  fvelimab 3756  ssimaex 3759  tfrlem4 3905  abianfp 3953  oprvalelrn 4030  mapsn 4335  php 4499  php3 4501  ssfi 4521  domfi 4522  unifi 4538  fiint 4540  fodomfi 4546  fodomfib 4547  iunfi 4549  pwfi 4551  inf0 4586  inf3lemd 4592  inf3lem6 4598  trcl 4625  rankr1 4654  bndrank 4662  rankc2 4686  rankxpsuc 4695  scott0 4697  aceq5lem4 4718  aceq6b 4722  ac6lem 4734  weth 4767  zorn2lem7 4774  cardiun 4839  cardalephex 4866  isinfcard 4867  alephfp 4880  cnegextlem2 5326  negeu 5335  receu 5678  infmrcl 6024  bndndx 6028  elq 6203  om2uzran 6245  limsupclt 6470  sqrlem20 6630  cau5i 6862  cvg1 6866  cvg3 6868  caubnd 6871  climshft 7049  caucvglem2 7102  caucvg3lem 7110  cvgcmpub 7129  infcvgaux1 7162  ruclem33 7493  ruclem35 7495  infxpidmlem12 7514  retopbas 7605  ntrss2 7640  ssnei 7674  opnneiid 7687  sncld 7737  caun0 7896  minveclem10 8498  circgrp 8679  projlem8 9132  projlem15 9139  pjth 9171  h1de2ctlem 9417  h1de2ct 9418  spansn 9419  spanunsn 9442  nmcopexlem6 9894  nmcfnexlem6 9923  riesz3 9933  adjbd1o 9956  rnbra 9978  pjnmop 10013  atom1d 10217  cvexchlem 10232  cdj1 10294  cdj3lem1 10295  ghomgrpilem2 10320  homcard 10462  fgsb 10480  efilcp 10481  fgsb2 10485  efilcp2 10486

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain