Theorem ralimi 2168

Description: Inference quantifying both antecedent and consequent, with strong hypothesis.

Hypothesis

Ref	Expression
ralimi.1	|- (ph -> ps)

Assertion

Ref	Expression
ralimi	|- (A.x e. A ph -> A.x e. A ps)

Proof of Theorem ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 |- (ph -> ps)
2	1	a1i 8	. 2 |- (x e. A -> (ph -> ps))
3	2	ralimia 2166	1 |- (A.x e. A ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 1300  A.wral 2105

This theorem is referenced by:  ral2imi 2169  r19.26 2219  r19.29 2227  reu3 2444  uniss2 3209  ss2iun 3271  iineq2 3274  iunss2 3298  truni 3425  eufromeq2 3829  eufromeq3 3830  eufromeq6 3833  tfis 3938  findOLD 3978  dffun8OLD 4449  fununi 4481  fun11uni 4483  zfrep6 4545  fnopabg 4546  elrnopabg 4773  dffo5 4794  fopab2 4796  elrnoprabg 5066  unifi2 5649  iunfi 5659  rankonid 5806  aceq5 5902  ac5b 5915  ac6lem 5916  ac6 5917  kmlem6 5932  kmlem8 5934  kmlem13 5939  xrsupexmnf 7283  xrinfmexpnf 7284  cau3iri 8167  cau3i 8168  cvganz 8176  2sumeq2dv 8254  fsum1s 8269  fsump1s 8273  fsumadd 8282  csbfsum 8287  fsummulc1 8293  fsumcmp 8300  fsumcmp0 8301  fsumcmpndx2 8302  fsumabs 8303  fsumabs2mul 8304  serzmulc1 8317  clm3i 8339  clmi2i 8347  clm0ii 8349  climunii 8358  2climnn 8362  2climnn0 8363  climge0 8372  climabs0i 8373  iserzmulc1 8396  climcmplem 8397  climsqueeze 8400  climsqueeze2 8401  iserzcmp 8402  caucvg3i 8427  iserzgt0 8472  explecnv 8495  basgen2 8909  bastop1 8912  neips 9003  cncnp 9055  meteq0 9089  mettri2 9090  mettri4 9091  lmcvg2 9211  caun0 9223  xplm 9253  iscms2 9272  isgrp 9321  grpidinv 9332  grpideu 9333  grprlidrid 9337  grpidinv2 9344  ringideu 9470  ringdi 9471  ringdir 9472  ringass 9473  vcid 9502  vcdi 9503  vcdir 9504  vcass 9505  nvs 9622  nvz 9629  nvtri 9630  ajmoi 9860  laspwcl 10011  lanfwcl 10012  grothpw 10134  grothpwex 10135  grothomex 10136  axgroth3 10138  fipreima 10175  opidon 10369  exidu1 10373  grpmnd 10393  rngmgmbs4 10401  uznzr 10416  projlem22 10840  adjmo 11395  adjvalval 11498  lnopconi 11600  lnfnconi 11627  cnlnssadj 11650  stge0 11796  stle1 11797  mdbr3 11869  mdbr4 11870  mdsl1i 11893  dmdbr6ati 11995  dmdbr7ati 11996  bnj899 12816  bnj1498 13562  ndvdssub 13710  truniOLD 13792  untangtr 13802  elpotr 13847  dfon2lem7 13855  dfon2lem8 13856  tfisg 13912  wfisg 13917  frinsg 13941  frxp 13951  poseq 13954  domfldrefc 14361  ranfldrefc 14362  domintrefb 14367  ref4w 14370  celsor 14443  surjsec2 14467  fopab2g 14485  mapmapmap 14486  dstr 14516  labs1 14536  labs2 14538  fprod1s 14677  fprodp1s 14682  fprodadd 14713  fnopabco2b 14734  fprodsub 14742  fldax3 14779  fldax4 14780  fldax5 14781  vecax3 14798  vecax4 14799  vecax5 14800  vecax6 14801  svli2 14826  supbrr 15048  imonclem 15162  iepiclem 15172  tarax1 15216  tarax2 15217  intartar 15255  tartarmap 15265  topbasfne 15499  neibastop1 15518  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2 15523  fipreimaOLD 15756  frinfm 15758  zornn0 15764  sdclem1 15809  fsum00 15820  fsumlt 15821  fsumlt1 15831  sstotbnd 15936  heiborlem23 15977  pcohtpy 16083  rnghomadd 16123  rnghommul 16124  idladdcl 16167  idllmulcl 16168  idlrmulcl 16169  ispridl2 16186  ralbidar 16422  rexbidar 16423  grpidinvNEW 17113  grpideuNEW 17114  grpidinv2NEW 17119  ringideuNEW 17146  pmapglbx 17251

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-ral 2109

Copyright terms: Public domain