Theorem r19.23adv 1743

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

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

Assertion

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

Distinct variable groups:   ph,x   ch,x

Proof of Theorem r19.23adv

Step	Hyp	Ref	Expression
1		ax-17 969	. 2 |- (ph -> A.xph)
2		ax-17 969	. 2 |- (ch -> A.xch)
3		r19.23adv.1	. 2 |- (ph -> (x e. A -> (ps -> ch)))
4	1, 2, 3	r19.23ad 1742	1 |- (ph -> (E.x e. A ps -> ch))

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

This theorem is referenced by:  r19.23adva 1744  r19.23advv 1746  elpwunsn 2907  tz7.7 2968  ssorduni 2988  onint 3001  limuni3 3118  funcnvuni 3556  dffo3 3810  isofrlem 3892  tfrlem9 3910  oaordex 4182  oalimcl 4184  oaass 4185  omlimcl 4199  odi 4200  finsucdom 4512  unblem1 4523  inf3lem3 4595  noinfep 4620  tz9.12lem3 4641  karden 4706  aceq5lem4 4718  aceq5 4720  cardaleph 4865  cardinfima 4871  alephval2 4882  cnegext 5328  recext 5665  nndivt 5914  btwnz 6171  uzwo3lem1 6172  qbtwnre 6224  fsequb 6463  seq1ublem 6856  caubnd 6871  clm3 7025  climsup 7099  caucvglem2 7102  caucvglem4 7104  caucvg3lem 7110  serzf0 7113  ser1f0 7114  unbenlem 7455  unitgt 7573  tgclt 7574  tgss2t 7587  subtop 7596  fctop 7600  cctop 7602  retopbas 7605  elcls 7654  elcls3 7661  islp2 7697  opni3 7818  opnuni 7820  neibl 7829  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metelcls 7916  metcnp4lem2 7919  cmsss 7947  bcthlem26 7974  bcthlem29 7977  grpidinvlem3 8000  grpidinvlem4 8001  grprcan 8013  isgrp2i 8026  grpinvf 8029  nmosetre 8372  nmoubi 8380  isblo3i 8405  blocnilem 8408  ubthlem14 8486  efifolem4 8659  projlem13 9137  omlsi 9183  spansncol 9430  spansneleq 9432  spansneleqOLD 9433  spansnsst 9434  normcant 9439  pjspansnt 9440  spanunsn 9442  h1datom 9444  nmopsetretALT 9730  nmfnsetret 9744  nmopubt 9772  nmfnleubt 9788  nmcopexlem6 9894  lnopcon 9901  nmcfnexlem6 9923  lnfncon 9928  nlelch 9932  branmfnt 9976  cnvbravalt 9981  superpos 10218  chjatom 10221  cvbr3 10231  atoml 10246  trran 10516

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