ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimiva GIF 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 ((𝜑𝑥𝐴) → 𝜓)
Assertion
Ref Expression
ralrimiva (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3 ((𝜑𝑥𝐴) → 𝜓)
21ex 114 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2481 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1465  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  8685  creui  8686  suprzclex  9117  supinfneg  9358  infsupneg  9359  indstr2  9371  iooidg  9660  iccsupr  9717  icoshftf1o  9742  fznlem  9789  exfzdc  9985  exbtwnzlemstep  9993  exbtwnzlemex  9995  frec2uzrdg  10150  frecuzrdgrcl  10151  frecuzrdgtcl  10153  frecuzrdgsuc  10155  frecuzrdgrclt  10156  frecuzrdgg  10157  frecuzrdgfunlem  10160  frecuzrdgsuctlem  10164  iseqovex  10197  seq3val  10199  seqvalcd  10200  seq3-1  10201  seqf  10202  seq3p1  10203  seqovcd  10204  seqp1cd  10207  seq3clss  10208  seq3fveq2  10210  seq3fveq  10212  seq3feq  10213  seq3shft2  10214  monoord  10217  monoord2  10218  ser3mono  10219  seq3split  10220  seq3caopr3  10222  seq3caopr2  10223  iseqf1olemqk  10235  iseqf1olemjpcl  10236  iseqf1olemqpcl  10237  iseqf1olemfvp  10238  seq3f1olemqsumkj  10239  seq3f1olemqsumk  10240  seq3f1olemqsum  10241  seq3f1oleml  10244  seq3f1o  10245  seq3id3  10248  seq3id  10249  seq3id2  10250  seq3homo  10251  seq3z  10252  ser3ge0  10258  bccl  10481  hashinfuni  10491  hashennnuni  10493  shftf  10570  seq3shft  10578  caucvgrelemcau  10720  cvg1nlemcau  10724  cvg1nlemres  10725  resqrexlemcvg  10759  resqrexlemglsq  10762  resqrexlemga  10763  maxabslemval  10948  negfi  10967  minmax  10969  xrmaxiflemval  10987  xrminmax  11002  climconst  11027  2clim  11038  climcn1  11045  climcn2  11046  reccn2ap  11050  cn1lem  11051  climsqz  11072  climsqz2  11073  climcau  11084  climrecvg1n  11085  serf0  11089  sumeq2dv  11105  sumrbdclem  11113  fsum3cvg  11114  summodclem3  11117  summodclem2a  11118  zsumdc  11121  isum  11122  fsumgcl  11123  fsum3  11124  fsumf1o  11127  isumss  11128  fisumss  11129  isumss2  11130  fsum3cvg2  11131  fsumsersdc  11132  fsum3ser  11134  fsumcl2lem  11135  fsumadd  11143  fsumsplit  11144  fsumm1  11153  fsum1p  11155  isumclim3  11160  isummulc2  11163  sumsplitdc  11169  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fsummulc2  11185  fsumge1  11198  fsum00  11199  fsumabs  11202  telfsumo  11203  telfsumo2  11204  fsumparts  11207  fsumrelem  11208  fsumiun  11214  hashiun  11215  hash2iun  11216  binomlem  11220  isumshft  11227  isum1p  11229  isumnn0nn  11230  isumrpcl  11231  isumlessdc  11233  divcnv  11234  cvgratnnlemnexp  11261  cvgratnnlemmn  11262  cvgratnnlemseq  11263  cvgratnnlemabsle  11264  cvgratnnlemfm  11266  cvgratnnlemrate  11267  cvgratnn  11268  cvgratz  11269  mertenslemi1  11272  mertenslem2  11273  mertensabs  11274  efcvgfsum  11300  dvdsssfz1  11477  zsupcllemstep  11565  infssuzex  11569  dvdsbnd  11572  bezoutlemstep  11612  bezoutlemmain  11613  bezoutlemle  11623  bezoutlemsup  11624  dfgcd3  11625  dfgcd2  11629  coprmgcdb  11696  isprm6  11752  phivalfi  11815  phibndlem  11819  dfphi2  11823  hashdvds  11824  phiprmpw  11825  phimullem  11828  hashgcdeq  11831  ennnfonelemex  11854  ennnfonelemfun  11857  ennnfonelemf1  11858  ennnfonelemnn0  11862  ennnfonelemim  11864  exmidunben  11866  ctinfomlemom  11867  ctinfom  11868  ctinf  11870  ctiunctlemudc  11877  ctiunctlemf  11878  ctiunctlemfo  11879  fiinbas  12143  tgclb  12161  restbasg  12264  iscnp4  12314  cnco  12317  cnptopco  12318  cnss1  12322  cnss2  12323  cncnpi  12324  cncnp  12326  cnconst2  12329  cnrest  12331  cnptopresti  12334  cnpdis  12338  lmtopcnp  12346  txbasval  12363  tx1cn  12365  tx2cn  12366  txcnp  12367  upxp  12368  txdis1cn  12374  cnmpt11  12379  psmet0  12423  psmettri2  12424  psmetxrge0  12428  psmetres2  12429  ismeti  12442  xmetpsmet  12465  blsscls2  12589  comet  12595  xmettx  12606  tgioo  12642  tgqioo  12643  fsumcncntop  12652  elcncf1di  12662  cdivcncfap  12683  mulcncflem  12686  mulcncf  12687  cnopnap  12690  dedekindeulemuub  12691  dedekindeulemlu  12695  suplociccreex  12698  suplociccex  12699  dedekindicclemuub  12700  dedekindicclemlu  12704  ivthinclemlopn  12710  ivthinclemlr  12711  ivthinclemuopn  12712  ivthinclemur  12713  ivthinclemdisj  12714  ivthinclemloc  12715  ivthinc  12717  ivthdec  12718  cnplimclemr  12734  limccnp2cntop  12742  limccoap  12743  dvcn  12760  dvfre  12770  dvrecap  12773  dvmptclx  12776  dvmptaddx  12777  dvmptmulx  12778  dveflem  12782  dvef  12783  sin0pilem1  12789  sin0pilem2  12790  nnsf  13126  nninfalllemn  13129  nninfalllem1  13130  nninfall  13131  nninfself  13136  nninfsellemeq  13137  nninfsellemeqinf  13139  nninfsel  13140  isomninnlem  13152  trilpolemeq1  13160  trilpo  13163
  Copyright terms: Public domain W3C validator