Theorem r19.21adv 2181

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 1317	. 2 |- (ph -> A.xph)
2		ax-17 1317	. 2 |- (ps -> A.xps)
3		r19.21adv.1	. 2 |- (ph -> (ps -> (x e. A -> ch)))
4	1, 2, 3	r19.21ad 2180	1 |- (ph -> (ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  r19.21adva 2182  r19.21aivv 2183  wefrc 3652  ralxfrd 3837  oneqmin 3886  isocnv 4873  isotr 4874  f1oiso 4881  tfrlem1 5119  abianfp 5171  omsmo 5314  mapenlem2 5584  nneneq 5606  cflim 6057  nnleltp1 7138  infmrcl 7278  supxrunb2 7299  zmax 7433  zbtwnre 7434  fzrevral 7698  sqr2irrlem3 7976  seq1ublem 8163  cau3iri 8167  clm4lei 8341  climconsti 8354  climshfti 8364  climcaui 8416  caucvglem2 8418  caucvgi 8423  expcnvlem6 8493  topbas 8897  clsval2 8961  elcls3 8987  neips 9003  clslp 9024  cnpnei 9043  cncnp 9055  opnuni 9145  opnin 9146  lmnn 9213  metcnp4 9248  xplmi 9251  bcthlem21 9297  isgrp2i 9360  gaid 9454  ipblnfi 9857  fbfgss 10288  hausfillim 10303  flimopn 10321  cncomp 10331  hial0 10601  hial02 10602  ocsh 10789  ococss 10799  occllem6 10811  projlem26 10844  pjtheui 10868  lnopmi 11562  adjlnop 11656  bra11 11679  pjss2coi 11736  pj3cor1i 11782  strlem3a 11824  hstrlem3a 11832  mdbr3 11869  mdbr4 11870  dmdmd 11872  dmdbr3 11877  dmdbr4 11878  dmdbr5 11880  ssmd2 11884  mdslmd1i 11901  mdsymlem7 11981  cdj1i 12005  cdj3lem2b 12009  ghomf1olem 13637  ublbneg 13653  cncls 15419  cnntr 15420  cnsubsp2 15427  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  alexsublem4 15440  alexsub 15441  isfne3 15482  comppfsc 15517  fnejoin1 15530  ist1-2 15542  ist1-3 15543  isufil2 15565  limfilcf 15587  flimcls 15588  cnpfillim 15589  fclusnei 15607  fclusbas 15610  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomp 15621  ufcomp 15622  fclusfnei 15626  raleqfn 15672  lmtlm 15908  isgrpda 16033  isringd 16097  trintALT 16705  hlrelat2 17052  pointpsub 17231  pmaple 17241

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain