ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimiva Unicode version

Theorem ralrimiva 2482
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
ralrimiva.1  |-  ( (
ph  /\  x  e.  A )  ->  ps )
Assertion
Ref Expression
ralrimiva  |-  ( ph  ->  A. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ps )
21ex 114 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2481 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1465   A.wral 2393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-4 1472  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  ralrimivvva  2492  rgen2  2495  rgen3  2496  nrexdv  2502  r19.29vva  2554  rabbidva  2648  ssrabdv  3146  ss2rabdv  3148  iuneq2dv  3804  disjeq2dv  3881  mpteq12dva  3979  triun  4009  issod  4211  frirrg  4242  frind  4244  peano2  4479  dmmptd  5223  fun11iun  5356  fniinfv  5447  eqfnfv  5486  eqfnfvd  5489  dff3im  5533  dffo4  5536  fmptd  5542  ffnfv  5546  fmpt2d  5550  ffvresb  5551  fconst2g  5603  fconstfvm  5606  resfunexg  5609  eufnfv  5616  foco2  5623  fniunfv  5631  fcofo  5653  fliftel  5662  fliftfun  5665  fliftfuns  5667  riota5f  5722  grprinvlem  5933  grprinvd  5934  f1ocnvd  5940  suppssov1  5947  offval2  5965  ofrfval2  5966  offveqb  5969  caofref  5971  caofinvl  5972  opabex3d  5987  oprssdmm  6037  f1od2  6100  disjxp1  6101  tfrlem1  6173  tfrlemisucaccv  6190  tfrlemiubacc  6195  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemubacc  6211  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemubacc  6224  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  rdgon  6251  freccllem  6267  frecfcllem  6269  omcl  6325  oeicl  6326  qliftfuns  6481  ixpeq2dva  6575  xpf1o  6706  mapxpen  6710  isinfinf  6759  fimax2gtrilemstep  6762  undifdcss  6779  eqsuptid  6852  eqinftid  6876  difinfsnlem  6952  difinfsn  6953  ctmlemr  6961  ctm  6962  ctssdclemn0  6963  ctssdccl  6964  enumctlemm  6967  enomnilem  6978  nnnninf  6991  ismkvnex  6997  acfun  7031  exmidaclem  7032  ccfunen  7047  genprndl  7297  genprndu  7298  nqprloc  7321  ltexprlemrnd  7381  ltexprlemdisj  7382  lteupri  7393  recexprlemrnd  7405  recexprlemdisj  7406  caucvgprlemlim  7457  caucvgprprlemlim  7487  suplocexprlemml  7492  suplocexprlemrl  7493  suplocexprlemmu  7494  suplocexprlemru  7495  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  caucvgsrlembound  7570  caucvgsrlemgt1  7571  caucvgsrlemoffgt1  7575  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  elrealeu  7605  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  negeu  7921  eqord1  8213  eqord2  8214  creur  8681  creui  8682  suprzclex  9107  supinfneg  9346  infsupneg  9347  indstr2  9359  iooidg  9647  iccsupr  9704  icoshftf1o  9729  fznlem  9776  exfzdc  9972  exbtwnzlemstep  9980  exbtwnzlemex  9982  frec2uzrdg  10137  frecuzrdgrcl  10138  frecuzrdgtcl  10140  frecuzrdgsuc  10142  frecuzrdgrclt  10143  frecuzrdgg  10144  frecuzrdgfunlem  10147  frecuzrdgsuctlem  10151  iseqovex  10184  seq3val  10186  seqvalcd  10187  seq3-1  10188  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3clss  10195  seq3fveq2  10197  seq3fveq  10199  seq3feq  10200  seq3shft2  10201  monoord  10204  monoord2  10205  ser3mono  10206  seq3split  10207  seq3caopr3  10209  seq3caopr2  10210  iseqf1olemqk  10222  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsumk  10227  seq3f1olemqsum  10228  seq3f1oleml  10231  seq3f1o  10232  seq3id3  10235  seq3id  10236  seq3id2  10237  seq3homo  10238  seq3z  10239  ser3ge0  10245  bccl  10468  hashinfuni  10478  hashennnuni  10480  shftf  10557  seq3shft  10565  caucvgrelemcau  10707  cvg1nlemcau  10711  cvg1nlemres  10712  resqrexlemcvg  10746  resqrexlemglsq  10749  resqrexlemga  10750  maxabslemval  10935  negfi  10954  minmax  10956  xrmaxiflemval  10974  xrminmax  10989  climconst  11014  2clim  11025  climcn1  11032  climcn2  11033  reccn2ap  11037  cn1lem  11038  climsqz  11059  climsqz2  11060  climcau  11071  climrecvg1n  11072  serf0  11076  sumeq2dv  11092  sumrbdclem  11100  fsum3cvg  11101  summodclem3  11104  summodclem2a  11105  zsumdc  11108  isum  11109  fsumgcl  11110  fsum3  11111  fsumf1o  11114  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsumsersdc  11119  fsum3ser  11121  fsumcl2lem  11122  fsumadd  11130  fsumsplit  11131  fsumm1  11140  fsum1p  11142  isumclim3  11147  isummulc2  11150  sumsplitdc  11156  fsum2dlemstep  11158  fisumcom2  11162  fsumshftm  11169  fsummulc2  11172  fsumge1  11185  fsum00  11186  fsumabs  11189  telfsumo  11190  telfsumo2  11191  fsumparts  11194  fsumrelem  11195  fsumiun  11201  hashiun  11202  hash2iun  11203  binomlem  11207  isumshft  11214  isum1p  11216  isumnn0nn  11217  isumrpcl  11218  isumlessdc  11220  divcnv  11221  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemseq  11250  cvgratnnlemabsle  11251  cvgratnnlemfm  11253  cvgratnnlemrate  11254  cvgratnn  11255  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  efcvgfsum  11287  dvdsssfz1  11462  zsupcllemstep  11550  infssuzex  11554  dvdsbnd  11557  bezoutlemstep  11597  bezoutlemmain  11598  bezoutlemle  11608  bezoutlemsup  11609  dfgcd3  11610  dfgcd2  11614  coprmgcdb  11681  isprm6  11737  phivalfi  11799  phibndlem  11803  dfphi2  11807  hashdvds  11808  phiprmpw  11809  phimullem  11812  hashgcdeq  11815  ennnfonelemex  11838  ennnfonelemfun  11841  ennnfonelemf1  11842  ennnfonelemnn0  11846  ennnfonelemim  11848  exmidunben  11850  ctinfomlemom  11851  ctinfom  11852  ctinf  11854  ctiunctlemudc  11861  ctiunctlemf  11862  ctiunctlemfo  11863  fiinbas  12127  tgclb  12145  restbasg  12248  iscnp4  12298  cnco  12301  cnptopco  12302  cnss1  12306  cnss2  12307  cncnpi  12308  cncnp  12310  cnconst2  12313  cnrest  12315  cnptopresti  12318  cnpdis  12322  lmtopcnp  12330  txbasval  12347  tx1cn  12349  tx2cn  12350  txcnp  12351  upxp  12352  txdis1cn  12358  cnmpt11  12363  psmet0  12407  psmettri2  12408  psmetxrge0  12412  psmetres2  12413  ismeti  12426  xmetpsmet  12449  blsscls2  12573  comet  12579  xmettx  12590  tgioo  12626  tgqioo  12627  fsumcncntop  12636  elcncf1di  12646  cdivcncfap  12667  mulcncflem  12670  mulcncf  12671  cnopnap  12674  dedekindeulemuub  12675  dedekindeulemlu  12679  suplociccreex  12682  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemlu  12688  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemdisj  12698  ivthinclemloc  12699  ivthinc  12701  ivthdec  12702  cnplimclemr  12718  limccnp2cntop  12726  limccoap  12727  dvcn  12744  dvfre  12754  dvrecap  12757  dvmptclx  12760  dvmptaddx  12761  dvmptmulx  12762  dveflem  12766  dvef  12767  sin0pilem1  12773  sin0pilem2  12774  nnsf  13095  nninfalllemn  13098  nninfalllem1  13099  nninfall  13100  nninfself  13105  nninfsellemeq  13106  nninfsellemeqinf  13108  nninfsel  13109  isomninnlem  13121  trilpolemeq1  13129  trilpo  13132
  Copyright terms: Public domain W3C validator