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

Theorem ralrimiva 2509
 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 2508 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481  ∀wral 2417 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422 This theorem is referenced by:  ralrimivvva  2519  rgen2  2522  rgen3  2523  nrexdv  2529  r19.29vva  2581  rabbidva  2678  ssrabdv  3182  ss2rabdv  3184  iuneq2dv  3843  disjeq2dv  3920  mpteq12dva  4018  triun  4048  issod  4250  frirrg  4281  frind  4283  peano2  4518  dmmptd  5262  fun11iun  5397  fniinfv  5488  eqfnfv  5527  eqfnfvd  5530  dff3im  5574  dffo4  5577  fmptd  5583  ffnfv  5587  fmpt2d  5591  ffvresb  5592  fconst2g  5644  fconstfvm  5647  resfunexg  5650  eufnfv  5657  foco2  5664  fniunfv  5672  fcofo  5694  fliftel  5703  fliftfun  5706  fliftfuns  5708  riota5f  5763  grprinvlem  5974  grprinvd  5975  f1ocnvd  5981  suppssov1  5988  offval2  6006  ofrfval2  6007  offveqb  6010  caofref  6012  caofinvl  6013  opabex3d  6028  oprssdmm  6078  f1od2  6141  disjxp1  6142  tfrlem1  6214  tfrlemisucaccv  6231  tfrlemiubacc  6236  tfr1onlemsucfn  6246  tfr1onlemsucaccv  6247  tfr1onlembxssdm  6249  tfr1onlembfn  6250  tfr1onlemubacc  6252  tfr1onlemaccex  6254  tfr1onlemres  6255  tfrcllemsucfn  6259  tfrcllemsucaccv  6260  tfrcllembxssdm  6262  tfrcllembfn  6263  tfrcllemubacc  6265  tfrcllemaccex  6267  tfrcllemres  6268  tfrcl  6270  rdgon  6292  freccllem  6308  frecfcllem  6310  omcl  6366  oeicl  6367  qliftfuns  6522  ixpeq2dva  6616  xpf1o  6747  mapxpen  6751  isinfinf  6800  fimax2gtrilemstep  6803  undifdcss  6821  eqsuptid  6894  eqinftid  6918  difinfsnlem  6994  difinfsn  6995  ctmlemr  7003  ctm  7004  ctssdclemn0  7005  ctssdccl  7006  enumctlemm  7009  enomnilem  7020  nnnninf  7033  ismkvnex  7039  enmkvlem  7045  enwomnilem  7053  acfun  7083  exmidaclem  7084  pw1on  7097  ccfunen  7116  cc2lem  7118  cc3  7120  genprndl  7373  genprndu  7374  nqprloc  7397  ltexprlemrnd  7457  ltexprlemdisj  7458  lteupri  7469  recexprlemrnd  7481  recexprlemdisj  7482  caucvgprlemlim  7533  caucvgprprlemlim  7563  suplocexprlemml  7568  suplocexprlemrl  7569  suplocexprlemmu  7570  suplocexprlemru  7571  suplocexprlemdisj  7572  suplocexprlemloc  7573  suplocexprlemub  7575  caucvgsrlembound  7646  caucvgsrlemgt1  7647  caucvgsrlemoffgt1  7651  caucvgsr  7654  suplocsrlemb  7658  suplocsrlempr  7659  suplocsrlem  7660  elrealeu  7681  axcaucvglemcau  7750  axcaucvglemres  7751  axpre-suploclemres  7753  negeu  7997  eqord1  8289  eqord2  8290  creur  8761  creui  8762  suprzclex  9193  supinfneg  9437  infsupneg  9438  indstr2  9450  iooidg  9742  iccsupr  9799  icoshftf1o  9824  fznlem  9872  exfzdc  10068  exbtwnzlemstep  10076  exbtwnzlemex  10078  frec2uzrdg  10233  frecuzrdgrcl  10234  frecuzrdgtcl  10236  frecuzrdgsuc  10238  frecuzrdgrclt  10239  frecuzrdgg  10240  frecuzrdgfunlem  10243  frecuzrdgsuctlem  10247  iseqovex  10280  seq3val  10282  seqvalcd  10283  seq3-1  10284  seqf  10285  seq3p1  10286  seqovcd  10287  seqp1cd  10290  seq3clss  10291  seq3fveq2  10293  seq3fveq  10295  seq3feq  10296  seq3shft2  10297  monoord  10300  monoord2  10301  ser3mono  10302  seq3split  10303  seq3caopr3  10305  seq3caopr2  10306  iseqf1olemqk  10318  iseqf1olemjpcl  10319  iseqf1olemqpcl  10320  iseqf1olemfvp  10321  seq3f1olemqsumkj  10322  seq3f1olemqsumk  10323  seq3f1olemqsum  10324  seq3f1oleml  10327  seq3f1o  10328  seq3id3  10331  seq3id  10332  seq3id2  10333  seq3homo  10334  seq3z  10335  ser3ge0  10341  bccl  10565  hashinfuni  10575  hashennnuni  10577  shftf  10654  seq3shft  10662  caucvgrelemcau  10804  cvg1nlemcau  10808  cvg1nlemres  10809  resqrexlemcvg  10843  resqrexlemglsq  10846  resqrexlemga  10847  maxabslemval  11032  negfi  11051  minmax  11053  xrmaxiflemval  11071  xrminmax  11086  climconst  11111  2clim  11122  climcn1  11129  climcn2  11130  reccn2ap  11134  cn1lem  11135  climsqz  11156  climsqz2  11157  climcau  11168  climrecvg1n  11169  serf0  11173  sumeq2dv  11189  sumrbdclem  11198  fsum3cvg  11199  summodclem3  11201  summodclem2a  11202  zsumdc  11205  isum  11206  fsumgcl  11207  fsum3  11208  fsumf1o  11211  isumss  11212  fisumss  11213  isumss2  11214  fsum3cvg2  11215  fsumsersdc  11216  fsum3ser  11218  fsumcl2lem  11219  fsumadd  11227  fsumsplit  11228  fsumm1  11237  fsum1p  11239  isumclim3  11244  isummulc2  11247  sumsplitdc  11253  fsum2dlemstep  11255  fisumcom2  11259  fsumshftm  11266  fsummulc2  11269  fsumge1  11282  fsum00  11283  fsumabs  11286  telfsumo  11287  telfsumo2  11288  fsumparts  11291  fsumrelem  11292  fsumiun  11298  hashiun  11299  hash2iun  11300  binomlem  11304  isumshft  11311  isum1p  11313  isumnn0nn  11314  isumrpcl  11315  isumlessdc  11317  divcnv  11318  cvgratnnlemnexp  11345  cvgratnnlemmn  11346  cvgratnnlemseq  11347  cvgratnnlemabsle  11348  cvgratnnlemfm  11350  cvgratnnlemrate  11351  cvgratnn  11352  cvgratz  11353  mertenslemi1  11356  mertenslem2  11357  mertensabs  11358  clim2prod  11360  prodeq2dv  11387  prodrbdclem  11392  fproddccvg  11393  prodmodclem3  11396  prodmodclem2a  11397  zproddc  11400  iprodap  11401  fprodseq  11404  efcvgfsum  11430  dvdsssfz1  11606  zsupcllemstep  11694  infssuzex  11698  dvdsbnd  11701  bezoutlemstep  11741  bezoutlemmain  11742  bezoutlemle  11752  bezoutlemsup  11753  dfgcd3  11754  dfgcd2  11758  coprmgcdb  11825  isprm6  11881  phivalfi  11944  phibndlem  11948  dfphi2  11952  hashdvds  11953  phiprmpw  11954  phimullem  11957  hashgcdeq  11960  ennnfonelemex  11983  ennnfonelemfun  11986  ennnfonelemf1  11987  ennnfonelemnn0  11991  ennnfonelemim  11993  exmidunben  11995  ctinfomlemom  11996  ctinfom  11997  ctinf  11999  ctiunctlemudc  12006  ctiunctlemf  12007  ctiunctlemfo  12008  omctfn  12012  fiinbas  12275  tgclb  12293  restbasg  12396  iscnp4  12446  cnco  12449  cnptopco  12450  cnss1  12454  cnss2  12455  cncnpi  12456  cncnp  12458  cnconst2  12461  cnrest  12463  cnptopresti  12466  cnpdis  12470  lmtopcnp  12478  txbasval  12495  tx1cn  12497  tx2cn  12498  txcnp  12499  upxp  12500  txdis1cn  12506  cnmpt11  12511  psmet0  12555  psmettri2  12556  psmetxrge0  12560  psmetres2  12561  ismeti  12574  xmetpsmet  12597  blsscls2  12721  comet  12727  xmettx  12738  tgioo  12774  tgqioo  12775  fsumcncntop  12784  elcncf1di  12794  cdivcncfap  12815  mulcncflem  12818  mulcncf  12819  cnopnap  12822  dedekindeulemuub  12823  dedekindeulemlu  12827  suplociccreex  12830  suplociccex  12831  dedekindicclemuub  12832  dedekindicclemlu  12836  ivthinclemlopn  12842  ivthinclemlr  12843  ivthinclemuopn  12844  ivthinclemur  12845  ivthinclemdisj  12846  ivthinclemloc  12847  ivthinc  12849  ivthdec  12850  cnplimclemr  12866  limccnp2cntop  12874  limccoap  12875  dvcn  12892  dvfre  12902  dvrecap  12905  dvmptclx  12908  dvmptaddx  12909  dvmptmulx  12910  dveflem  12915  dvef  12916  sin0pilem1  12930  sin0pilem2  12931  pw1nct  13390  nnsf  13393  nninfalllemn  13396  nninfalllem1  13397  nninfall  13398  nninfself  13403  nninfsellemeq  13404  nninfsellemeqinf  13406  nninfsel  13407  isomninnlem  13419  trilpolemeq1  13429  trilpo  13432  apdiff  13437  iswomninnlem  13438  iswomni0  13440  ismkvnnlem  13441  redcwlpo  13444  redc0  13446  reap0  13447  dceqnconst  13448  dcapnconst  13449  nconstwlpolem  13453  nconstwlpo  13454  neapmkv  13456
 Copyright terms: Public domain W3C validator