Theorem 19.23aiv 1297

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

Syntax hints:   -> wi 3  E.wex 982

This theorem is referenced by:  19.23aivv 1298  mo 1395  mopick 1435  zfext2 1464  gencl 1831  cgsexg 1834  gencbvex2 1842  vtocleg 1858  eqvinc 1886  uniiunlem 2136  eluni 2511  axsep2 2710  bm1.3ii 2712  intex 2735  unipw 2763  moabex 2773  nnullss 2775  exss 2776  mosubopt 2811  ssopab2 2829  reuunisn 2902  limuni3 3130  findsg 3164  tfindsg 3169  relop 3282  dmrnssfld 3364  elxp5 3461  unixp0 3525  ffoss 3718  fvopabn 3793  exfo 3829  tfrlem8 3925  tfrlem9 3926  fnoprabg 4019  erref 4282  ectocl 4309  ecoptocl 4310  mapprc 4333  map0b 4350  map0 4351  uniixp 4364  breng 4382  brdomg 4383  ener 4417  en0 4430  en1 4433  2dom 4434  undom 4445  xpdom2 4449  xpdom3 4452  pw2en 4453  mapen 4498  mapdom1 4499  mapdom2 4501  ssenen 4511  php 4520  0sdom1dom 4532  unfilem1 4562  unifi 4572  unifiOLD 4574  fodomfi 4582  fodomfiOLD 4583  pm54.43 4588  inf3 4636  infeq5 4637  omex 4643  zfregs 4664  tz9.12lem1 4676  bnd2 4741  aceq3lem 4749  aceq4 4751  aceq5lem4 4755  aceq5lem5 4756  aceq5 4757  aceq6a 4758  aceq6b 4759  ac6lem 4771  ac6s 4773  kmlem2 4783  kmlem16 4797  numthlem 4800  weth 4804  brdom3 4818  brdom5 4819  brdom4 4820  brdom7disj 4821  brdom6disj 4822  unidom 4825  oncard 4846  carduni 4876  cardcf 4930  cfeq0 4933  cfsuc 4934  cfom 4935  ltbtwnpq 5103  ltaprlem 5169  reclem1pr 5175  reclem2pr 5176  reclem3pr 5177  map2psrpr 5239  supsrlem2 5245  suprelem 5278  renegcl 5435  0re 5459  redivcl 5807  nnunb 6079  isumshft 7211  isumshft2 7212  acdc3 7495  acdc2 7498  acdc5 7501  acdc 7503  infxpidmlem4 7563  infxpidmlem7 7566  infxpidmlem10 7569  infxpidmlem12 7571  infpss 7582  infmap2lem2 7589  tgval3t 7631  eltg3t 7632  bastop 7648  isgrp2i 8079  minvecex 8581  projlem 9219  shintcl 9295  pjrn 9649  strlem1 10180  uninqs 10444  infi1 10449  fine 10450  fiiu 10452  ficli 10470  fiv 10478  fiiu2 10481  inposet 10485  homcard 10533  fisub 10566  infi 10567  rcfpfillem2 10572  rcfpfillem3 10573  rcfpfillem4 10574  rcfpfillem6 10576  rcfpfil 10577

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain