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

Theorem ralrimiva 2446
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 113 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2445 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  ralrimivvva  2456  rgen2  2459  rgen3  2460  nrexdv  2466  r19.29vva  2513  rabbidva  2607  ssrabdv  3098  ss2rabdv  3100  iuneq2dv  3746  disjeq2dv  3819  mpteq12dva  3911  triun  3941  issod  4137  frirrg  4168  frind  4170  peano2  4400  fun11iun  5258  fniinfv  5346  eqfnfv  5381  eqfnfvd  5384  dff3im  5428  dffo4  5431  fmptd  5436  ffnfv  5440  fmpt2d  5444  ffvresb  5445  fconst2g  5494  fconstfvm  5497  resfunexg  5500  eufnfv  5507  foco2  5515  fniunfv  5523  fcofo  5545  fliftel  5554  fliftfun  5557  fliftfuns  5559  riota5f  5614  grprinvlem  5821  grprinvd  5822  f1ocnvd  5828  suppssov1  5835  offval2  5852  ofrfval2  5853  offveqb  5856  caofref  5858  caofinvl  5859  opabex3d  5874  f1od2  5982  disjxp1  5983  tfrlem1  6055  tfrlemisucaccv  6072  tfrlemiubacc  6077  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemubacc  6093  tfr1onlemaccex  6095  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemubacc  6106  tfrcllemaccex  6108  tfrcllemres  6109  tfrcl  6111  rdgon  6133  freccllem  6149  frecfcllem  6151  omcl  6204  oeicl  6205  qliftfuns  6356  xpf1o  6540  mapxpen  6544  isinfinf  6593  fimax2gtrilemstep  6596  undifdcss  6613  eqsuptid  6671  eqinftid  6695  enomnilem  6773  nnnninf  6785  genprndl  7059  genprndu  7060  nqprloc  7083  ltexprlemrnd  7143  ltexprlemdisj  7144  lteupri  7155  recexprlemrnd  7167  recexprlemdisj  7168  caucvgprlemlim  7219  caucvgprprlemlim  7249  caucvgsrlembound  7318  caucvgsrlemgt1  7319  caucvgsrlemoffgt1  7323  caucvgsr  7326  elrealeu  7346  axcaucvglemcau  7412  axcaucvglemres  7413  negeu  7652  creur  8391  creui  8392  suprzclex  8814  supinfneg  9052  infsupneg  9053  indstr2  9065  iooidg  9296  iccsupr  9353  icoshftf1o  9377  fznlem  9424  exfzdc  9616  exbtwnzlemstep  9624  exbtwnzlemex  9626  frec2uzrdg  9781  frecuzrdgrcl  9782  frecuzrdgtcl  9784  frecuzrdgsuc  9786  frecuzrdgrclt  9787  frecuzrdgg  9788  frecuzrdgfunlem  9791  frecuzrdgsuctlem  9795  iseqovex  9835  iseqval  9836  iseqvalt  9838  seq3val  9839  iseq1  9840  iseq1t  9841  seq3-1  9842  iseqfcl  9843  iseqfclt  9844  seqf  9845  iseqcl  9846  iseqp1  9847  iseqp1t  9848  seq3p1  9849  iseqoveq  9850  seq3clss  9852  iseqfveq2  9855  seq3fveq2  9857  iseqfveq  9859  seq3fveq  9860  iseqfeq  9861  seq3feq  9862  iseqshft2  9863  monoord  9869  monoord2  9870  isermono  9871  seq3split  9872  iseqsplit  9873  iseqcaopr3  9875  iseqcaopr2  9876  iseqf1olemqk  9888  iseqf1olemjpcl  9889  iseqf1olemqpcl  9890  iseqf1olemfvp  9891  seq3f1olemqsumkj  9892  seq3f1olemqsumk  9893  seq3f1olemqsum  9894  seq3f1oleml  9897  seq3f1o  9898  iseqid3s  9903  iseqid  9904  seq3id2  9905  iseqid2  9906  iseqhomo  9907  iseqz  9908  seq3homo  9909  ser3ge0  9917  bccl  10140  hashinfuni  10150  hashennnuni  10152  shftf  10229  seq3shft  10237  caucvgrelemcau  10378  cvg1nlemcau  10382  cvg1nlemres  10383  resqrexlemcvg  10417  resqrexlemglsq  10420  resqrexlemga  10421  maxabslemval  10606  negfi  10623  minmax  10625  climconst  10642  2clim  10653  climcn1  10661  climcn2  10662  cn1lem  10666  climsqz  10687  climsqz2  10688  climcau  10700  climrecvg1n  10701  serif0  10705  sumeq2dv  10721  isumrblem  10729  fisumcvg  10730  fsum3cvg  10731  isummolem3  10734  isummolem2a  10735  zisum  10738  iisum  10739  fsumgcl  10741  fisum  10742  fsumf1o  10746  isumss  10747  fisumss  10748  isumss2  10749  fisumcvg2  10750  fisumsers  10751  fisumser  10753  fsumcl2lem  10755  fsumadd  10763  fsumsplit  10764  fsumm1  10773  fsum1p  10775  isumclim3  10780  isummulc2  10783  sumsplitdc  10789  fsum2dlemstep  10791  fisumcom2  10795  fsumshftm  10802  fsummulc2  10805  fsumge1  10818  fsum00  10819  fsumabs  10822  telfsumo  10823  telfsumo2  10824  fsumparts  10827  fsumrelem  10828  fsumiun  10833  hashiun  10834  hash2iun  10835  binomlem  10839  isumshft  10846  isum1p  10848  isumnn0nn  10849  isumrpcl  10850  divcnv  10852  cvgratnnlemnexp  10879  cvgratnnlemmn  10880  cvgratnnlemseq  10881  cvgratnnlemabsle  10882  cvgratnnlemfm  10884  cvgratnnlemrate  10885  cvgratnn  10886  cvgratz  10887  dvdsssfz1  10946  zsupcllemstep  11034  infssuzex  11038  dvdsbnd  11041  bezoutlemstep  11079  bezoutlemmain  11080  bezoutlemle  11090  bezoutlemsup  11091  dfgcd3  11092  dfgcd2  11096  coprmgcdb  11163  isprm6  11219  phivalfi  11281  phibndlem  11285  dfphi2  11289  hashdvds  11290  phiprmpw  11291  phimullem  11294  hashgcdeq  11297  nnsf  11552  nninfalllemn  11555  nninfalllem1  11556  nninfall  11557  nninfself  11562  nninfsellemeq  11563  nninfsellemeqinf  11565  nninfsel  11566
  Copyright terms: Public domain W3C validator