Theorem r19.21adv 1765

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

Hypothesis

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

Assertion

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

Distinct variable groups:   ph,x   ps,x

Proof of Theorem r19.21adv

Step	Hyp	Ref	Expression
1		ax-17 1012	. 2 |- (ph -> A.xph)
2		ax-17 1012	. 2 |- (ps -> A.xps)
3		r19.21adv.1	. 2 |- (ph -> (ps -> (x e. A -> ch)))
4	1, 2, 3	r19.21ad 1764	1 |- (ph -> (ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 999  A.wral 1692

This theorem is referenced by:  r19.21adva 1766  r19.21aivv 1767  ralxfrd 2954  wefrc 3000  oneqmin 3075  isocnv 3954  isotr 3955  f1oiso 3962  tfrlem1 3969  abianfp 4020  omsmo 4315  mapenlem2 4555  nneneq 4577  cflim 4974  nnleltp1 6015  infmrcl 6151  supxrunb2 6172  zmax 6305  zbtwnre 6306  fzrevral 6545  sqr2irrlem3 6816  seq1ublem 7001  cau3iri 7005  clm4lei 7171  climconsti 7184  climshfti 7194  climcaui 7246  caucvglem2 7248  caucvgi 7253  expcnvlem6 7322  topbas 7716  clsval2 7770  elcls3 7796  neips 7812  clslp 7833  cncnp 7863  opnuni 7953  opnin 7954  lmnn 8020  metcnp4 8055  xplmi 8058  bcthlem21 8104  isgrp2i 8160  ipblnfi 8600  hial0 9051  hial02 9052  ocsh 9239  ococss 9249  occllem6 9261  projlem26 9294  pjtheui 9318  lnopmi 10008  adjlnop 10102  bra11 10124  pjss2coi 10175  pj3cor1i 10221  strlem3a 10263  hstrlem3a 10271  mdbr3 10308  mdbr4 10309  dmdmd 10311  dmdbr3 10316  dmdbr4 10317  dmdbr5 10319  ssmd2 10323  mdslmd1i 10340  mdsymlem7 10420  cdj1i 10444  cdj3lem2b 10448  ghomf1olem 10481

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019

This theorem depends on definitions:  df-bi 154  df-an 232  df-ral 1696

Copyright terms: Public domain