Theorem r19.23aiv 1284

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(s):   ps,x

Proof of Theorem r19.23aiv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ps -> A.xps)
2		r19.23aiv.1	. 2 |- (x e. A -> (ph -> ps))
3	1, 2	r19.23ai 1283	1 |- (E.x e. A ph -> ps)

Syntax hints:   -> wi 2   e. wcel 1092  E.wrex 1202

This theorem is referenced by:  r19.23aivv 1287  r19.36av 1299  r19.44av 1305  r19.45av 1306  uniss2 1942  eliun 1998  frirr 2176  fr2nr 2177  fr3nr 2178  unon 2338  onuninsuc 2356  ordzsl 2366  onzsl 2367  fvelrn 2883  tfrlem4 2952  tfrlem8 2956  abianfp 3000  oawordeulem 3156  mapsn 3269  php 3409  php3 3411  ominf 3423  isfinite1 3425  ssfi 3430  fiint 3445  inf0 3457  inf3lemd 3463  inf3lem6 3469  trcl 3489  rankr1 3518  bndrank 3526  scott0 3542  aceq5lem4 3561  aceq6b 3565  ac6lem 3575  weth 3602  zornlem7 3609  cardiun 3665  cardalephex 3691  isinfcard 3692  addcan 4120  negeu 4124  mulcan 4207  receu 4215  elq 4629  om2uzran 4655  sqrlem20 4750  ruclem33 4917  ruclem35 4919  infxpidmlem12 4944  projlem8 5200  projlem15 5207  pjth 5239  h1de2ctlem 5460  h1de2ct 5461  spansn 5462  spanunsn 5482  str 5698  stcltrth 5711  atom1d 5750  shatomic 5753  cvexchlem 5759

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-rex 1206

metamath.org