Theorem 19.23aiv 1674

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 1317	. 2 |- (ps -> A.xps)
2		19.23aiv.1	. 2 |- (ph -> ps)
3	1, 2	19.23ai 1412	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  E.wex 1326

This theorem is referenced by:  19.23aivv 1675  mo 1787  mopick 1833  axext3OLD 1868  gencl 2318  cgsexg 2321  gencbvex2 2336  vtocleg 2355  eqvinc 2387  eqvincOLD 2388  uniiunlem 2693  eluni 3180  uniintsn 3253  axsep2 3439  bm1.3ii 3441  intex 3465  axpweq 3480  eunex 3500  unipw 3504  moabex 3513  nnullss 3515  exss 3516  mosubopt 3551  ssopab2 3573  reuunisn 3822  limuni3 3936  tfindsg 3944  findsg 3980  relop 4113  dmrnssfld 4205  dmsnop 4367  elxp5 4380  unixp0 4423  ffoss 4665  dffv2 4734  fvopabn 4749  exfo 4795  fnoprabg 4941  fo1stres 5036  fo2ndres 5037  iotaequ 5097  iota4 5100  tfrlem8 5126  tfrlem9 5127  erref 5333  mapprc 5385  map0b 5402  map0 5403  uniixp 5416  breng 5434  brdomg 5435  ener 5469  en0 5482  en1 5485  2dom 5486  fiprc 5492  undom 5497  xpdom2 5501  xpdom3 5504  pw2en 5505  ac6sfi 5509  mapen 5585  mapdom1 5586  mapdom2 5588  ssenen 5598  php 5607  0sdom1dom 5618  unfilem1 5641  unifi 5648  fodomfi 5656  pm54.43 5662  inf3 5726  infeq5 5727  omex 5733  zfregs 5754  tz9.12lem1 5770  bnd2 5854  aceq3lem 5894  aceq4 5896  aceq5lem4 5900  aceq5lem5 5901  aceq5 5902  aceq6a 5903  aceq6b 5904  ac6lem 5916  ac6s 5918  kmlem2 5928  kmlem16 5942  numthlem 5945  weth 5949  brdom3 5963  brdom5 5964  brdom4 5965  brdom7disj 5966  brdom6disj 5967  unidom 5970  oncard 5978  carduni 6010  cardcf 6059  cfeq0 6062  cfsuc 6063  cfom 6064  ltbtwnpq 6236  ltaprlem 6302  reclem1pr 6308  reclem2pr 6309  reclem3pr 6310  map2psrpr 6372  supsrlem2 6378  suprelem 6411  renegcliOLD 6577  0re 6603  redivcli 6976  nnunb 7279  isumshfti 8465  isumshft2i 8466  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  infxpidmlem4 8824  infxpidmlem7 8827  infxpidmlem10 8830  infxpidmlem12 8832  infpss 8843  infmap2lem2 8849  tgval3 8895  eltg3 8896  bastop1 8912  subbas2 8915  isgrp2i 9360  isga 9450  gapm 9462  minvecex 9923  grothpw 10134  grothpwex 10135  oprabopabf 10157  fiv 10212  fine 10213  fiiu2 10220  fbssint 10279  infi 10280  filrn 10293  projlem 10850  shintcli 10926  pjrni 11282  strlem1 11822  bnj521 12522  bnj578 13291  bnj605 13292  bnj607 13304  bnj1018 13378  bnj1020 13379  bnj1145 13431  ordsucuniel 13863  frxp 13951  wfrlem2 13958  wfrlem3 13959  wfrlem4 13960  wfrlem9 13965  wfrlem12 13968  txpss3v 14065  brtxp 14067  elfix 14077  uninqs 14340  infi1 14343  fiiu 14344  ficli 14353  f1fi 14377  prj1 14395  injrec2 14466  surjsec2 14467  cbicplem 14508  prl 14512  inposet 14620  osneisi 14875  homcard 14893  fisub 14924  rcfpfillem2 14929  rcfpfillem3 14930  rcfpfillem4 14931  rcfpfillem6 14933  rcfpfil 14934  bwt2 14960  domleqt 15020  emptar 15231  intrtael 15256  compsub 15431  hscptsscld 15434  compfipin0 15436  alexsublem2 15438  alexsub 15441  reconn 15451  isfne3 15482  topmtcl 15525  fcluscomplem 15620  filnetlem1 15640  prfOLD 15680  fimax 15746  indexdom 15754  heiborlem11 15965  heiborlem13 15967  heiborlem40 15994  iotain 16381  iotavalb 16394  euunianOLD 16396  sbiota1 16399  ipo0 16426  ifr0 16427  trint0 16439

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

Copyright terms: Public domain