Theorem r19.23aiv 2211

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

Syntax hints:   -> wi 3   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  r19.23aiva 2212  r19.23aivv 2217  r19.36av 2232  r19.44av 2240  r19.45av 2241  rexn0 2972  uniss2 3209  eliun 3259  frirr 3634  fr2nr 3635  fr3nr 3859  onuninsuci 3921  ordzsl 3927  onzsl 3928  onzslOLD 3929  fvelrnb 4719  fvelimab 4725  fvelimabOLD 4726  ssimaex 4729  oprvelrn 4969  tfrlem4 5122  abianfp 5171  ectocl 5361  ecoptocl 5362  mapsn 5404  isfi 5441  ac6sfi 5509  php 5607  php3 5609  ssfi 5630  unifi 5648  fiint 5650  fodomfi 5656  iunfi 5659  pwfi 5661  inf0 5712  inf3lemd 5718  inf3lem6 5724  trcl 5752  rankr1 5785  bndrank 5793  rankc2 5817  rankxpsuc 5826  scott0 5847  aceq5lem4 5900  aceq6b 5904  ac6lem 5916  weth 5949  zorn2lem7 5956  cardiun 6011  cardalephex 6034  isinfcard 6035  alephfp 6048  cnegexlem2 6500  negeui 6510  renegcli 6576  receui 6890  infmrcl 7278  bndndx 7282  elq 7437  om2uzrani 7711  limsupcl 7773  sqrlem20 7942  cau5ii 8169  cvg1 8173  cvg3i 8175  caubndi 8178  climshfti 8364  caucvglem2 8418  caucvg3lem 8426  cvgcmpubi 8446  infcvgaux1i 8480  ruclem33 8811  ruclem35 8813  infxpidmlem12 8832  retopbas 8925  ntrss2 8966  ssnei 9000  opnneiid 9013  sncld 9064  caun0 9223  minveclem10 9899  circgrp 10094  indexfi 10174  fipreima 10175  findcard 10178  fbssint 10279  fgfil 10290  cncomp 10331  projlem8 10826  projlem15 10833  pjthi 10866  h1de2ctlem 11111  h1de2ci 11112  spansni 11113  spanunsni 11135  nmcopexlem6 11593  nmcfnexlem6 11622  riesz3i 11632  adjbd1o 11655  rnbra 11678  pjnmopi 11719  atom1d 11925  cvexchlem 11940  cdj1i 12005  cdj3lem1 12006  ghomgrpilem2 13629  ublbneg 13653  untint 13800  elres 13824  dfon2lem3 13851  dfon2lem7 13855  ordsucuniel 13863  orderseqlem 13953  elno 13987  nofun 13993  nodmon 13994  norn 13995  sltval2 13997  axbday 14012  axdenselem2 14020  axfelem15 14045  r19.23aivr 14294  uninqs 14340  prj1 14395  inpreima5 14469  nZdef 14527  grpdivfo 14737  zerdivemp1 14785  rngridfz 14786  svs2 14829  nsn 14874  homcard 14893  subspemp 14903  subtopsin2 14907  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  fbaslim2 14936  conttnf 14944  iscnp3 14946  bwt2 14960  altretoplem2 14996  cntrsetlem 14999  intartar 15255  finminlem 15367  finsschain 15373  compsublem 15430  hscptsscld 15434  is2ndc2 15473  2ndc1stc 15477  fneint 15486  neibastop1 15518  neibastop2 15523  uffixfr 15575  fclusbas 15610  unirep 15664  findcard2 15745  fimax 15746  indexfiOLD 15755  fipreimaOLD 15756  filbcmb 15776  sdc 15811  totbndbnd 15944  heiborlem7 15961  heiborlem10 15964  heiborlem11 15965  heiborlem23 15977  heiborlem39 15993  zerdivemp1x 16108  ispoint 17223  pmapglbx 17251

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain