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

Theorem ralrimiv 2961
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 1836 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 2950 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ral 2913
This theorem is referenced by:  ralrimiva  2962  ralrimivw  2963  ralrimdv  2964  ralrimivv  2966  reximdvai  3011  r19.27v  3065  raleleq  3149  rr19.3v  3333  rabssdv  3667  rzal  4051  trin  4733  class2seteq  4803  ralxfrALT  4857  otiunsndisj  4950  issref  5478  onmindif  5784  fnprb  6437  fntpb  6438  ssorduni  6947  onminex  6969  onmindif2  6974  suceloni  6975  limuni3  7014  frxp  7247  poxp  7249  wfrlem15  7389  onfununi  7398  onnseq  7401  tfrlem12  7445  tz7.48-2  7497  oaass  7601  omass  7620  oelim2  7635  oelimcl  7640  oaabs2  7685  omabs  7687  undifixp  7904  dom2lem  7955  isinf  8133  unblem4  8175  unbnn2  8177  marypha1lem  8299  supiso  8341  ordiso2  8380  card2inf  8420  elirrv  8464  wemapwe  8554  trcl  8564  tz9.13  8614  rankval3b  8649  rankunb  8673  rankuni2b  8676  scott0  8709  dfac8alem  8812  carduniima  8879  alephsmo  8885  alephval3  8893  iunfictbso  8897  dfac3  8904  dfac5lem5  8910  dfac12r  8928  dfac12k  8929  kmlem4  8935  kmlem11  8942  cfsuc  9039  cofsmo  9051  cfsmolem  9052  coftr  9055  alephsing  9058  infpssrlem3  9087  fin23lem30  9124  isf32lem2  9136  isf32lem3  9137  isf34lem6  9162  fin1a2lem11  9192  fin1a2lem13  9194  fin1a2s  9196  axcc2lem  9218  domtriomlem  9224  axdc3lem2  9233  axdc4lem  9237  axcclem  9239  axdclem2  9302  iundom2g  9322  uniimadom  9326  cardmin  9346  alephval2  9354  alephreg  9364  fpwwe2lem12  9423  wunex2  9520  wuncval2  9529  tskwe2  9555  inar1  9557  tskuni  9565  gruun  9588  intgru  9596  grutsk1  9603  genpcl  9790  ltexprlem5  9822  suplem1pr  9834  supexpr  9836  supsrlem  9892  axpre-sup  9950  fiminre  10932  supaddc  10950  supadd  10951  supmul1  10952  supmullem1  10953  supmul  10955  peano5nni  10983  uzind  11429  zindd  11438  uzwo  11711  lbzbi  11736  xrsupsslem  12096  xrinfmsslem  12097  supxrun  12105  supxrpnf  12107  supxrunb1  12108  supxrunb2  12109  icoshftf1o  12253  flval3  12572  axdc4uzlem  12738  ccatrn  13327  2cshw  13512  cshweqrep  13520  s3iunsndisj  13657  rtrclreclem4  13751  dfrtrcl2  13752  sqrlem1  13933  sqrlem6  13938  fsum0diag2  14462  alzdvds  14985  gcdcllem1  15164  lcmfunsnlem2lem1  15294  lcmfunsnlem2lem2  15295  maxprmfct  15364  hashgcdeq  15437  unbenlem  15555  vdwlem6  15633  vdwlem10  15637  firest  16033  mrieqv2d  16239  iscatd  16274  setcmon  16677  setcepi  16678  fullestrcsetc  16731  fullsetcestrc  16746  isglbd  17057  isacs4lem  17108  acsfiindd  17117  acsmapd  17118  psss  17154  ghmrn  17613  ghmpreima  17622  cntz2ss  17705  symgextres  17785  psgnunilem2  17855  lsmsubg  18009  efgsfo  18092  gsumzaddlem  18261  gsummptnn0fzfv  18324  dmdprdd  18338  dprd2da  18381  imasring  18559  isabvd  18760  issrngd  18801  islssd  18876  lbsextlem3  19100  lbsextlem4  19101  lidldvgen  19195  psgnghm  19866  isphld  19939  frlmsslsp  20075  mp2pm2mplem4  20554  tgcl  20713  distop  20739  indistopon  20745  pptbas  20752  toponmre  20837  opnnei  20864  neiuni  20866  neindisj2  20867  ordtrest2  20948  cnpnei  21008  cnindis  21036  cmpcld  21145  uncmp  21146  hauscmplem  21149  2ndc1stc  21194  1stcrest  21196  1stcelcls  21204  llyrest  21228  nllyrest  21229  cldllycmp  21238  reftr  21257  locfincf  21274  comppfsc  21275  txcls  21347  ptpjcn  21354  ptclsg  21358  dfac14lem  21360  xkoccn  21362  txlly  21379  txnlly  21380  ptrescn  21382  tx1stc  21393  xkoco1cn  21400  xkoco2cn  21401  xkococn  21403  xkoinjcn  21430  qtopeu  21459  hmeofval  21501  ordthmeolem  21544  isfild  21602  fbasrn  21628  trfil2  21631  flimclslem  21728  fclsrest  21768  fclscf  21769  flimfcls  21770  alexsubALTlem1  21791  alexsubALTlem2  21792  alexsubALTlem3  21793  alexsubALT  21795  qustgpopn  21863  isxmetd  22071  imasdsf1olem  22118  blcls  22251  prdsxmslem2  22274  metustfbas  22302  dscmet  22317  nrmmetd  22319  reperflem  22561  reconnlem2  22570  xrge0tsms  22577  fsumcn  22613  cnheibor  22694  tchcph  22976  lmmbr  22996  caubl  23046  ivthlem1  23160  ovolctb  23198  ovoliunlem2  23211  ovolscalem1  23221  ovolicc2  23230  voliunlem3  23260  ismbfd  23347  mbfimaopnlem  23362  itg2le  23446  ellimc2  23581  c1liplem1  23697  plyeq0lem  23904  dgreq0  23959  aannenlem1  24021  pilem2  24144  cxpcn3lem  24422  scvxcvx  24646  musum  24851  dchrisum0flb  25133  ostth2lem2  25257  nbuhgr  26160  nbumgr  26164  uhgrnbgr0nb  26171  uvtxanbgrvtx  26214  cusgrfilem2  26273  uspgr2wlkeq  26445  wwlks  26630  2wspiundisj  26758  rusgr0edg  26769  clwwisshclwwslem  26827  3cyclfrgrrn  27048  vdgn1frgrv3  27059  numclwlk2lem2f1o  27127  frgrregord013  27141  htthlem  27662  ocsh  28030  shintcli  28076  pjss2coi  28911  pjnormssi  28915  pjclem4  28946  pj3si  28954  pj3cor1i  28956  strlem3a  28999  strb  29005  hstrlem3a  29007  hstrbi  29013  spansncv2  29040  mdsl1i  29068  cvmdi  29071  mdexchi  29082  h1da  29096  mdsymlem6  29155  sumdmdii  29162  dmdbr5ati  29169  isoun  29363  supssd  29371  infssd  29372  xrge0tsmsd  29612  ordtrest2NEW  29793  pwsiga  30016  measiun  30104  dya2iocuni  30168  bnj518  30717  bnj1137  30824  bnj1136  30826  bnj1413  30864  bnj1417  30870  bnj60  30891  erdszelem8  30941  cvmsss2  31017  cvmfolem  31022  dfon2lem8  31449  dfon2lem9  31450  dfon2  31451  rdgprc  31454  trpredtr  31484  trpredmintr  31485  trpredelss  31486  dftrpred3g  31487  trpredpo  31489  trpredrec  31492  frr3g  31533  frrlem5b  31539  frrlem5d  31541  sltval2  31563  nosires  31630  nn0prpwlem  32012  ntruni  32017  clsint2  32019  fneint  32038  fnessref  32047  refssfne  32048  neibastop1  32049  neibastop2lem  32050  relowlpssretop  32883  heicant  33115  mblfinlem1  33117  ftc2nc  33165  sdclem2  33209  fdc  33212  seqpo  33214  prdsbnd  33263  heibor  33291  rrnequiv  33305  0idl  33495  intidl  33499  unichnidl  33501  prnc  33537  lsmcv2  33835  lcvexchlem4  33843  lcvexchlem5  33844  eqlkr  33905  paddclN  34647  pclfinN  34705  ldilcnv  34920  ldilco  34921  cdleme25dN  35163  cdlemj2  35629  tendocan  35631  erng1lem  35794  erngdvlem4-rN  35806  dihord2pre  36033  dihglblem2N  36102  dochvalr  36165  hdmap14lem12  36690  hdmap14lem13  36691  pellfundre  36964  pellfundge  36965  pellfundlb  36967  dford3lem1  37112  aomclem2  37144  pwinfi3  37388  iunrelexp0  37514  iunrelexpmin1  37520  iunrelexpmin2  37524  dftrcl3  37532  cnvtrclfv  37536  trclimalb2  37538  dfrtrcl3  37545  ntrneiel2  37905  ntrneik4w  37919  ntrrn  37941  gneispa  37949  gneispb  37950  addrcom  38200  iunconnlem2  38693  ssuzfz  39064  dvmptfprod  39497  dvnprodlem3  39500  funressnfv  40542  tz6.12-afv  40587  otiunsndisjX  40625  iccpartltu  40689  iccpartgtl  40690  iccpartleu  40692  iccpartgel  40693  fargshiftf  40704  fargshiftfva  40707  bgoldbst  40991  bgoldbtbnd  41016  tgblthelfgott  41020  tgblthelfgottOLD  41027  nnsgrp  41135  ellcoellss  41542  lindsrng01  41575  suppdm  41618  nn0sumshdiglem1  41737  ssdifsn  41752  setrec2fun  41762
  Copyright terms: Public domain W3C validator