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

Theorem ralrimiva 2480
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 2479 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1463   A.wral 2391
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  ralrimivvva  2490  rgen2  2493  rgen3  2494  nrexdv  2500  r19.29vva  2552  rabbidva  2646  ssrabdv  3144  ss2rabdv  3146  iuneq2dv  3802  disjeq2dv  3879  mpteq12dva  3977  triun  4007  issod  4209  frirrg  4240  frind  4242  peano2  4477  dmmptd  5221  fun11iun  5354  fniinfv  5445  eqfnfv  5484  eqfnfvd  5487  dff3im  5531  dffo4  5534  fmptd  5540  ffnfv  5544  fmpt2d  5548  ffvresb  5549  fconst2g  5601  fconstfvm  5604  resfunexg  5607  eufnfv  5614  foco2  5621  fniunfv  5629  fcofo  5651  fliftel  5660  fliftfun  5663  fliftfuns  5665  riota5f  5720  grprinvlem  5931  grprinvd  5932  f1ocnvd  5938  suppssov1  5945  offval2  5963  ofrfval2  5964  offveqb  5967  caofref  5969  caofinvl  5970  opabex3d  5985  oprssdmm  6035  f1od2  6098  disjxp1  6099  tfrlem1  6171  tfrlemisucaccv  6188  tfrlemiubacc  6193  tfr1onlemsucfn  6203  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemubacc  6209  tfr1onlemaccex  6211  tfr1onlemres  6212  tfrcllemsucfn  6216  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemubacc  6222  tfrcllemaccex  6224  tfrcllemres  6225  tfrcl  6227  rdgon  6249  freccllem  6265  frecfcllem  6267  omcl  6323  oeicl  6324  qliftfuns  6479  ixpeq2dva  6573  xpf1o  6704  mapxpen  6708  isinfinf  6757  fimax2gtrilemstep  6760  undifdcss  6777  eqsuptid  6850  eqinftid  6874  difinfsnlem  6950  difinfsn  6951  ctmlemr  6959  ctm  6960  ctssdclemn0  6961  ctssdccl  6962  enumctlemm  6965  enomnilem  6976  nnnninf  6989  ismkvnex  6995  acfun  7027  exmidaclem  7028  ccfunen  7043  genprndl  7293  genprndu  7294  nqprloc  7317  ltexprlemrnd  7377  ltexprlemdisj  7378  lteupri  7389  recexprlemrnd  7401  recexprlemdisj  7402  caucvgprlemlim  7453  caucvgprprlemlim  7483  suplocexprlemml  7488  suplocexprlemrl  7489  suplocexprlemmu  7490  suplocexprlemru  7491  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  caucvgsrlembound  7566  caucvgsrlemgt1  7567  caucvgsrlemoffgt1  7571  caucvgsr  7574  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  elrealeu  7601  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  negeu  7917  eqord1  8209  eqord2  8210  creur  8674  creui  8675  suprzclex  9100  supinfneg  9339  infsupneg  9340  indstr2  9352  iooidg  9632  iccsupr  9689  icoshftf1o  9714  fznlem  9761  exfzdc  9957  exbtwnzlemstep  9965  exbtwnzlemex  9967  frec2uzrdg  10122  frecuzrdgrcl  10123  frecuzrdgtcl  10125  frecuzrdgsuc  10127  frecuzrdgrclt  10128  frecuzrdgg  10129  frecuzrdgfunlem  10132  frecuzrdgsuctlem  10136  iseqovex  10169  seq3val  10171  seqvalcd  10172  seq3-1  10173  seqf  10174  seq3p1  10175  seqovcd  10176  seqp1cd  10179  seq3clss  10180  seq3fveq2  10182  seq3fveq  10184  seq3feq  10185  seq3shft2  10186  monoord  10189  monoord2  10190  ser3mono  10191  seq3split  10192  seq3caopr3  10194  seq3caopr2  10195  iseqf1olemqk  10207  iseqf1olemjpcl  10208  iseqf1olemqpcl  10209  iseqf1olemfvp  10210  seq3f1olemqsumkj  10211  seq3f1olemqsumk  10212  seq3f1olemqsum  10213  seq3f1oleml  10216  seq3f1o  10217  seq3id3  10220  seq3id  10221  seq3id2  10222  seq3homo  10223  seq3z  10224  ser3ge0  10230  bccl  10453  hashinfuni  10463  hashennnuni  10465  shftf  10542  seq3shft  10550  caucvgrelemcau  10692  cvg1nlemcau  10696  cvg1nlemres  10697  resqrexlemcvg  10731  resqrexlemglsq  10734  resqrexlemga  10735  maxabslemval  10920  negfi  10939  minmax  10941  xrmaxiflemval  10959  xrminmax  10974  climconst  10999  2clim  11010  climcn1  11017  climcn2  11018  reccn2ap  11022  cn1lem  11023  climsqz  11044  climsqz2  11045  climcau  11056  climrecvg1n  11057  serf0  11061  sumeq2dv  11077  sumrbdclem  11085  fsum3cvg  11086  summodclem3  11089  summodclem2a  11090  zsumdc  11093  isum  11094  fsumgcl  11095  fsum3  11096  fsumf1o  11099  isumss  11100  fisumss  11101  isumss2  11102  fsum3cvg2  11103  fsumsersdc  11104  fsum3ser  11106  fsumcl2lem  11107  fsumadd  11115  fsumsplit  11116  fsumm1  11125  fsum1p  11127  isumclim3  11132  isummulc2  11135  sumsplitdc  11141  fsum2dlemstep  11143  fisumcom2  11147  fsumshftm  11154  fsummulc2  11157  fsumge1  11170  fsum00  11171  fsumabs  11174  telfsumo  11175  telfsumo2  11176  fsumparts  11179  fsumrelem  11180  fsumiun  11186  hashiun  11187  hash2iun  11188  binomlem  11192  isumshft  11199  isum1p  11201  isumnn0nn  11202  isumrpcl  11203  isumlessdc  11205  divcnv  11206  cvgratnnlemnexp  11233  cvgratnnlemmn  11234  cvgratnnlemseq  11235  cvgratnnlemabsle  11236  cvgratnnlemfm  11238  cvgratnnlemrate  11239  cvgratnn  11240  cvgratz  11241  mertenslemi1  11244  mertenslem2  11245  mertensabs  11246  efcvgfsum  11272  dvdsssfz1  11446  zsupcllemstep  11534  infssuzex  11538  dvdsbnd  11541  bezoutlemstep  11581  bezoutlemmain  11582  bezoutlemle  11592  bezoutlemsup  11593  dfgcd3  11594  dfgcd2  11598  coprmgcdb  11665  isprm6  11721  phivalfi  11783  phibndlem  11787  dfphi2  11791  hashdvds  11792  phiprmpw  11793  phimullem  11796  hashgcdeq  11799  ennnfonelemex  11822  ennnfonelemfun  11825  ennnfonelemf1  11826  ennnfonelemnn0  11830  ennnfonelemim  11832  exmidunben  11834  ctinfomlemom  11835  ctinfom  11836  ctinf  11838  ctiunctlemudc  11845  ctiunctlemf  11846  ctiunctlemfo  11847  fiinbas  12111  tgclb  12129  restbasg  12232  iscnp4  12282  cnco  12285  cnptopco  12286  cnss1  12290  cnss2  12291  cncnpi  12292  cncnp  12294  cnconst2  12297  cnrest  12299  cnptopresti  12302  cnpdis  12306  lmtopcnp  12314  txbasval  12331  tx1cn  12333  tx2cn  12334  txcnp  12335  upxp  12336  txdis1cn  12342  cnmpt11  12347  psmet0  12391  psmettri2  12392  psmetxrge0  12396  psmetres2  12397  ismeti  12410  xmetpsmet  12433  blsscls2  12557  comet  12563  xmettx  12574  tgioo  12610  tgqioo  12611  fsumcncntop  12620  elcncf1di  12630  cdivcncfap  12651  mulcncflem  12654  mulcncf  12655  cnopnap  12658  dedekindeulemuub  12659  dedekindeulemlu  12663  suplociccreex  12666  suplociccex  12667  dedekindicclemuub  12668  dedekindicclemlu  12672  cnplimclemr  12690  limccnp2cntop  12698  limccoap  12699  dvcn  12716  dvfre  12726  dvrecap  12729  dvmptclx  12732  dvmptaddx  12733  dvmptmulx  12734  dveflem  12738  dvef  12739  nnsf  13010  nninfalllemn  13013  nninfalllem1  13014  nninfall  13015  nninfself  13020  nninfsellemeq  13021  nninfsellemeqinf  13023  nninfsel  13024  isomninnlem  13036  trilpolemeq1  13044  trilpo  13047
  Copyright terms: Public domain W3C validator