MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimiv Structured version   Visualization version   GIF version

Theorem ralrimiv 3148
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.)
Hypothesis
Ref Expression
ralrimiv.1 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
ralrimiv (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiv
StepHypRef Expression
1 ax-5 1911 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 3147 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wral 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ral 3111
This theorem is referenced by:  ralrimiva  3149  ralrimivw  3150  ralrimdv  3153  ralrimivv  3155  reximdvai  3231  raleleq  3372  rr19.3v  3607  rabssdv  4002  rzal  4411  disjord  5018  disjiund  5020  trin  5146  class2seteq  5220  ralxfrALT  5281  otiunsndisj  5375  onmindif  6248  fnprb  6948  fntpb  6949  ssorduni  7480  onminex  7502  onmindif2  7507  suceloni  7508  limuni3  7547  frxp  7803  poxp  7805  wfrlem15  7952  onfununi  7961  onnseq  7964  tfrlem12  8008  tz7.48-2  8061  oaass  8170  omass  8189  oelim2  8204  oelimcl  8209  oaabs2  8255  omabs  8257  undifixp  8481  dom2lem  8532  isinf  8715  unblem4  8757  unbnn2  8759  marypha1lem  8881  supiso  8923  ordiso2  8963  card2inf  9003  elirrv  9044  wemapwe  9144  trcl  9154  tz9.13  9204  rankval3b  9239  rankunb  9263  rankuni2b  9266  scott0  9299  updjud  9347  dfac8alem  9440  carduniima  9507  alephsmo  9513  alephval3  9521  iunfictbso  9525  dfac3  9532  dfac5lem5  9538  dfac12r  9557  dfac12k  9558  kmlem4  9564  kmlem11  9571  cfsuc  9668  cofsmo  9680  cfsmolem  9681  coftr  9684  alephsing  9687  infpssrlem3  9716  fin23lem30  9753  isf32lem2  9765  isf32lem3  9766  isf34lem6  9791  fin1a2lem11  9821  fin1a2lem13  9823  fin1a2s  9825  axcc2lem  9847  domtriomlem  9853  axdc3lem2  9862  axdc4lem  9866  axcclem  9868  axdclem2  9931  iundom2g  9951  uniimadom  9955  cardmin  9975  alephval2  9983  alephreg  9993  fpwwe2lem12  10052  wunex2  10149  wuncval2  10158  tskwe2  10184  inar1  10186  tskuni  10194  gruun  10217  intgru  10225  grutsk1  10232  genpcl  10419  ltexprlem5  10451  suplem1pr  10463  supexpr  10465  supsrlem  10522  axpre-sup  10580  negfi  11577  supaddc  11595  supadd  11596  supmul1  11597  supmullem1  11598  supmul  11600  peano5nni  11628  uzind  12062  zindd  12071  uzwo  12299  lbzbi  12324  xrsupsslem  12688  xrinfmsslem  12689  supxrun  12697  supxrpnf  12699  supxrunb1  12700  supxrunb2  12701  icoshftf1o  12852  flval3  13180  axdc4uzlem  13346  wrdnfi  13891  ccatrn  13934  ccatalpha  13938  2cshw  14166  cshweqrep  14174  s3iunsndisj  14319  rtrclreclem4  14412  dfrtrcl2  14413  sqrlem1  14594  sqrlem6  14599  fsum0diag2  15130  alzdvds  15662  gcdcllem1  15838  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  maxprmfct  16043  hashgcdeq  16116  unbenlem  16234  vdwlem6  16312  vdwlem10  16316  firest  16698  mrieqv2d  16902  iscatd  16936  initoeu2  17268  setcmon  17339  setcepi  17340  fullestrcsetc  17393  fullsetcestrc  17408  isglbd  17719  isacs4lem  17770  acsfiindd  17779  acsmapd  17780  psss  17816  sgrpidmnd  17908  pwmnd  18094  ghmrn  18363  ghmpreima  18372  cntz2ss  18455  symgextres  18545  psgnunilem2  18615  lsmsubg  18771  efgsfo  18857  gsumzaddlem  19034  gsummptnn0fzfv  19100  dmdprdd  19114  dprd2da  19157  ablsimpgprmd  19230  imasring  19365  isabvd  19584  issrngd  19625  islssd  19700  lbsextlem3  19925  lbsextlem4  19926  lidldvgen  20021  psgnghm  20269  isphld  20343  frlmsslsp  20485  mp2pm2mplem4  21414  tgcl  21574  distop  21600  indistopon  21606  pptbas  21613  toponmre  21698  opnnei  21725  neiuni  21727  neindisj2  21728  ordtrest2  21809  cnpnei  21869  cnindis  21897  cmpcld  22007  uncmp  22008  hauscmplem  22011  2ndc1stc  22056  1stcrest  22058  1stcelcls  22066  llyrest  22090  nllyrest  22091  cldllycmp  22100  reftr  22119  locfincf  22136  comppfsc  22137  txcls  22209  ptpjcn  22216  ptclsg  22220  dfac14lem  22222  xkoccn  22224  txlly  22241  txnlly  22242  ptrescn  22244  tx1stc  22255  xkoco1cn  22262  xkoco2cn  22263  xkococn  22265  xkoinjcn  22292  qtopeu  22321  hmeofval  22363  ordthmeolem  22406  isfild  22463  fbasrn  22489  trfil2  22492  flimclslem  22589  fclsrest  22629  fclscf  22630  flimfcls  22631  alexsubALTlem1  22652  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALT  22656  qustgpopn  22725  isxmetd  22933  imasdsf1olem  22980  blcls  23113  prdsxmslem2  23136  metustfbas  23164  dscmet  23179  nrmmetd  23181  reperflem  23423  reconnlem2  23432  xrge0tsms  23439  fsumcn  23475  cnheibor  23560  tcphcph  23841  lmmbr  23862  caubl  23912  ivthlem1  24055  ovolctb  24094  ovoliunlem2  24107  ovolscalem1  24117  ovolicc2  24126  voliunlem3  24156  ismbfd  24243  mbfimaopnlem  24259  itg2le  24343  ellimc2  24480  c1liplem1  24599  plyeq0lem  24807  dgreq0  24862  aannenlem1  24924  pilem2  25047  cxpcn3lem  25336  scvxcvx  25571  musum  25776  dchrisum0flb  26094  ostth2lem2  26218  numedglnl  26937  upgrreslem  27094  umgrreslem  27095  nbuhgr  27133  nbumgr  27137  uhgrnbgr0nb  27144  nbusgrf1o0  27159  uvtxnbgrvtx  27183  cusgrfilem2  27246  uspgr2wlkeq  27435  wwlks  27621  iswwlksnon  27639  rusgr0edg  27759  clwwlkccatlem  27774  clwwisshclwwslem  27799  clwwlkn  27811  clwwlknon  27875  3cyclfrgrrn  28071  vdgn1frgrv3  28082  2wspmdisj  28122  numclwlk2lem2f1o  28164  frgrregord013  28180  htthlem  28700  ocsh  29066  shintcli  29112  pjss2coi  29947  pjnormssi  29951  pjclem4  29982  pj3si  29990  pj3cor1i  29992  strlem3a  30035  strb  30041  hstrlem3a  30043  hstrbi  30049  spansncv2  30076  mdsl1i  30104  cvmdi  30107  mdexchi  30118  h1da  30132  mdsymlem6  30191  sumdmdii  30198  dmdbr5ati  30205  isoun  30461  supssd  30471  infssd  30472  xrge0tsmsd  30742  ordtrest2NEW  31276  pwsiga  31499  measiun  31587  dya2iocuni  31651  bnj518  32268  bnj1137  32377  bnj1136  32379  bnj1413  32417  bnj1417  32423  bnj60  32444  subgrwlk  32492  erdszelem8  32558  cvmsss2  32634  cvmfolem  32639  fmlasucdisj  32759  satfun  32771  dfon2lem8  33148  dfon2lem9  33149  dfon2  33150  rdgprc  33152  trpredtr  33182  trpredmintr  33183  trpredelss  33184  dftrpred3g  33185  trpredpo  33187  trpredrec  33190  frr3g  33234  sltval2  33276  nolesgn2ores  33292  nosupres  33320  nosupbnd2lem1  33328  scutun12  33384  nn0prpwlem  33783  ntruni  33788  clsint2  33790  fneint  33809  fnessref  33818  refssfne  33819  neibastop1  33820  neibastop2lem  33821  bj-0int  34516  bj-ismooredr  34524  relowlpssretop  34781  fvineqsneu  34828  fvineqsneq  34829  heicant  35092  mblfinlem1  35094  ftc2nc  35139  sdclem2  35180  fdc  35183  seqpo  35185  prdsbnd  35231  heibor  35259  rrnequiv  35273  0idl  35463  intidl  35467  unichnidl  35469  prnc  35505  uniqsALTV  35746  lsmcv2  36325  lcvexchlem4  36333  lcvexchlem5  36334  eqlkr  36395  paddclN  37138  pclfinN  37196  ldilcnv  37411  ldilco  37412  cdleme25dN  37652  cdlemj2  38118  tendocan  38120  erng1lem  38283  erngdvlem4-rN  38295  dihord2pre  38521  dihglblem2N  38590  dochvalr  38653  hdmap14lem12  39175  hdmap14lem13  39176  fsuppind  39454  pellfundre  39820  pellfundge  39821  pellfundlb  39823  dford3lem1  39965  aomclem2  39997  pwinfi3  40260  iunrelexp0  40401  iunrelexpmin1  40407  iunrelexpmin2  40411  dftrcl3  40419  cnvtrclfv  40423  trclimalb2  40425  dfrtrcl3  40432  ntrneiel2  40787  ntrneik4w  40801  ntrrn  40823  gneispa  40831  gneispb  40832  addrcom  41177  iunconnlem2  41639  ssuzfz  41979  dvmptfprod  42585  dvnprodlem3  42588  funressnfv  43633  tz6.12-afv  43727  tz6.12-afv2  43794  otiunsndisjX  43833  uniimaprimaeqfv  43897  iccpartltu  43940  iccpartgtl  43941  iccpartleu  43943  iccpartgel  43944  fargshiftf  43955  fargshiftfva  43958  sbgoldbst  44294  bgoldbtbnd  44325  tgblthelfgott  44331  isomushgr  44342  nnsgrp  44435  ellcoellss  44842  lindsrng01  44875  suppdm  44917  nn0sumshdiglem1  45033  setrec2fun  45220
  Copyright terms: Public domain W3C validator