Theorem 19.23aiv 1290

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23aiv.1	|- (ph -> ps)

Assertion

Ref	Expression
19.23aiv	|- (E.xph -> ps)

Distinct variable group:   ps,x

Proof of Theorem 19.23aiv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ps -> A.xps)
2		19.23aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.23ai 1060	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  E.wex 977

This theorem is referenced by:  19.23aivv 1291  mo 1386  mopick 1426  zfext2 1454  gencl 1819  cgsexg 1822  gencbvex2 1830  vtocleg 1846  eqvinc 1874  uniiunlem 2122  eluni 2496  axsep2 2694  bm1.3ii 2696  intex 2719  unipw 2746  moabex 2756  nnullss 2758  exss 2759  mosubopt 2793  ssopab2 2811  reuunisn 2885  limuni3 3113  findsg 3147  tfindsg 3152  relop 3265  dmrnssfld 3343  elxp5 3440  unixp0 3504  ffoss 3696  fvopabn 3771  exfo 3807  tfrlem8 3903  tfrlem9 3904  fnoprabg 3997  erref 4259  ectocl 4286  ecoptocl 4287  mapprc 4310  map0b 4327  map0 4328  uniixp 4341  breng 4357  brdomg 4358  ener 4391  en0 4404  en1 4407  2dom 4408  undom 4418  xpdom2 4422  xpdom3 4425  pw2en 4426  mapen 4471  mapdom1 4472  mapdom2 4474  ssenen 4484  php 4493  0sdom1dom 4504  unfilem1 4524  unifi 4532  fodomfi 4540  pm54.43 4546  inf3 4592  infeq5 4593  omex 4599  zfregs 4619  tz9.12lem1 4631  bnd2 4696  aceq3lem 4704  aceq4 4706  aceq5lem4 4710  aceq5lem5 4711  aceq5 4712  aceq6a 4713  aceq6b 4714  ac6lem 4726  ac6s 4728  kmlem2 4738  kmlem16 4752  numthlem 4755  weth 4759  brdom3 4773  brdom5 4774  brdom4 4775  brdom7disj 4776  brdom6disj 4777  unidom 4780  oncard 4801  carduni 4830  cardcf 4883  cfeq0 4886  cfsuc 4887  cfom 4888  ltbtwnpq 5056  ltaprlem 5122  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  map2psrpr 5192  supsrlem2 5198  suprelem 5231  renegcl 5388  0re 5412  redivcl 5754  nnunb 6017  isumshft 7139  isumshft2 7140  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  infxpidmlem4 7498  infxpidmlem7 7501  infxpidmlem10 7504  infxpidmlem12 7506  infmap2lem2 7522  tgval3t 7567  eltg3t 7568  bastop 7584  subbas2 7587  isgrp2i 8011  minvecex 8509  projlem 9133  shintcl 9208  pjrn 9564  strlem1 10087  uninqs 10342  infi1 10347  fine 10348  fiiu 10350  ficli 10368  fiv 10374  fiiu2 10377  homcard 10426  fisub 10447  infi 10448

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain