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

Theorem ralrimiv 2948
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 1827 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 2937 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  ralrimiva  2949  ralrimivw  2950  ralrimdv  2951  ralrimivv  2953  reximdvai  2998  r19.27v  3052  raleleq  3133  rr19.3v  3314  rabssdv  3645  rzal  4025  trin  4691  class2seteq  4759  ralxfrALT  4813  otiunsndisj  4905  issref  5428  onmindif  5732  fnprb  6377  fntpb  6378  ssorduni  6877  onminex  6899  onmindif2  6904  suceloni  6905  limuni3  6944  frxp  7174  poxp  7176  wfrlem15  7316  onfununi  7325  onnseq  7328  tfrlem12  7372  tz7.48-2  7424  oaass  7528  omass  7547  oelim2  7562  oelimcl  7567  oaabs2  7612  omabs  7614  undifixp  7830  dom2lem  7881  isinf  8058  unblem4  8100  unbnn2  8102  marypha1lem  8222  supiso  8264  ordiso2  8303  card2inf  8343  elirrv  8387  wemapwe  8477  trcl  8487  tz9.13  8537  rankval3b  8572  rankunb  8596  rankuni2b  8599  scott0  8632  dfac8alem  8735  carduniima  8802  alephsmo  8808  alephval3  8816  iunfictbso  8820  dfac3  8827  dfac5lem5  8833  dfac12r  8851  dfac12k  8852  kmlem4  8858  kmlem11  8865  cfsuc  8962  cofsmo  8974  cfsmolem  8975  coftr  8978  alephsing  8981  infpssrlem3  9010  fin23lem30  9047  isf32lem2  9059  isf32lem3  9060  isf34lem6  9085  fin1a2lem11  9115  fin1a2lem13  9117  fin1a2s  9119  axcc2lem  9141  domtriomlem  9147  axdc3lem2  9156  axdc4lem  9160  axcclem  9162  axdclem2  9225  iundom2g  9241  uniimadom  9245  cardmin  9265  alephval2  9273  alephreg  9283  fpwwe2lem12  9342  wunex2  9439  wuncval2  9448  tskwe2  9474  inar1  9476  tskuni  9484  gruun  9507  intgru  9515  grutsk1  9522  genpcl  9709  ltexprlem5  9741  suplem1pr  9753  supexpr  9755  supsrlem  9811  axpre-sup  9869  fiminre  10851  supaddc  10867  supadd  10868  supmul1  10869  supmullem1  10870  supmul  10872  peano5nni  10900  uzind  11345  zindd  11354  uzwo  11627  lbzbi  11652  xrsupsslem  12009  xrinfmsslem  12010  supxrun  12018  supxrpnf  12020  supxrunb1  12021  supxrunb2  12022  icoshftf1o  12166  flval3  12478  axdc4uzlem  12644  ccatrn  13225  2cshw  13410  cshweqrep  13418  s3iunsndisj  13555  rtrclreclem4  13649  dfrtrcl2  13650  sqrlem1  13831  sqrlem6  13836  fsum0diag2  14357  alzdvds  14880  gcdcllem1  15059  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  maxprmfct  15259  hashgcdeq  15332  unbenlem  15450  vdwlem6  15528  vdwlem10  15532  firest  15916  mrieqv2d  16122  iscatd  16157  setcmon  16560  setcepi  16561  fullestrcsetc  16614  fullsetcestrc  16629  isglbd  16940  isacs4lem  16991  acsfiindd  17000  acsmapd  17001  psss  17037  ghmrn  17496  ghmpreima  17505  cntz2ss  17588  symgextres  17668  psgnunilem2  17738  lsmsubg  17892  efgsfo  17975  gsumzaddlem  18144  gsummptnn0fzfv  18207  dmdprdd  18221  dprd2da  18264  imasring  18442  isabvd  18643  issrngd  18684  islssd  18757  lbsextlem3  18981  lbsextlem4  18982  lidldvgen  19076  psgnghm  19745  isphld  19818  frlmsslsp  19954  mp2pm2mplem4  20433  tgcl  20584  distop  20610  indistopon  20615  pptbas  20622  toponmre  20707  opnnei  20734  neiuni  20736  neindisj2  20737  ordtrest2  20818  cnpnei  20878  cnindis  20906  cmpcld  21015  uncmp  21016  hauscmplem  21019  2ndc1stc  21064  1stcrest  21066  1stcelcls  21074  llyrest  21098  nllyrest  21099  cldllycmp  21108  reftr  21127  locfincf  21144  comppfsc  21145  txcls  21217  ptpjcn  21224  ptclsg  21228  dfac14lem  21230  xkoccn  21232  txlly  21249  txnlly  21250  ptrescn  21252  tx1stc  21263  xkoco1cn  21270  xkoco2cn  21271  xkococn  21273  xkoinjcn  21300  qtopeu  21329  hmeofval  21371  ordthmeolem  21414  isfild  21472  fbasrn  21498  trfil2  21501  flimclslem  21598  fclsrest  21638  fclscf  21639  flimfcls  21640  alexsubALTlem1  21661  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALT  21665  qustgpopn  21733  isxmetd  21941  imasdsf1olem  21988  blcls  22121  prdsxmslem2  22144  metustfbas  22172  dscmet  22187  nrmmetd  22189  reperflem  22429  reconnlem2  22438  xrge0tsms  22445  fsumcn  22481  cnheibor  22562  tchcph  22844  lmmbr  22864  caubl  22914  ivthlem1  23027  ovolctb  23065  ovoliunlem2  23078  ovolscalem1  23088  ovolicc2  23097  voliunlem3  23127  ismbfd  23213  mbfimaopnlem  23228  itg2le  23312  ellimc2  23447  c1liplem1  23563  plyeq0lem  23770  dgreq0  23825  aannenlem1  23887  pilem2  24010  cxpcn3lem  24288  scvxcvx  24512  musum  24717  dchrisum0flb  24999  ostth2lem2  25123  usgrares1  25939  nbusgra  25957  nbgra0nb  25958  nbgra0edg  25961  cusgrafilem2  26008  usgrasscusgra  26011  uvtxnbgravtx  26023  fargshiftf  26164  fargshiftfva  26167  usg2wlkeq  26236  clwwlkn0  26302  clwwisshclwwlem  26334  0egra0rgra  26463  eupatrl  26495  eupap1  26503  3cyclfrgrarn  26540  vdgn1frgrav3  26555  2spotiundisj  26589  numclwlk2lem2f1o  26632  frgraregord013  26645  htthlem  27158  ocsh  27526  shintcli  27572  pjss2coi  28407  pjnormssi  28411  pjclem4  28442  pj3si  28450  pj3cor1i  28452  strlem3a  28495  strb  28501  hstrlem3a  28503  hstrbi  28509  spansncv2  28536  mdsl1i  28564  cvmdi  28567  mdexchi  28578  h1da  28592  mdsymlem6  28651  sumdmdii  28658  dmdbr5ati  28665  isoun  28862  supssd  28870  infssd  28871  xrge0tsmsd  29116  ordtrest2NEW  29297  pwsiga  29520  measiun  29608  dya2iocuni  29672  bnj518  30210  bnj1137  30317  bnj1136  30319  bnj1413  30357  bnj1417  30363  bnj60  30384  erdszelem8  30434  cvmsss2  30510  cvmfolem  30515  dfon2lem8  30939  dfon2lem9  30940  dfon2  30941  rdgprc  30944  trpredtr  30974  trpredmintr  30975  trpredelss  30976  dftrpred3g  30977  trpredpo  30979  trpredrec  30982  frr3g  31023  frrlem5b  31029  frrlem5d  31031  sltval2  31053  nn0prpwlem  31487  ntruni  31492  clsint2  31494  fneint  31513  fnessref  31522  refssfne  31523  neibastop1  31524  neibastop2lem  31525  relowlpssretop  32388  heicant  32614  mblfinlem1  32616  ftc2nc  32664  sdclem2  32708  fdc  32711  seqpo  32713  prdsbnd  32762  heibor  32790  rrnequiv  32804  0idl  32994  intidl  32998  unichnidl  33000  prnc  33036  lsmcv2  33334  lcvexchlem4  33342  lcvexchlem5  33343  eqlkr  33404  paddclN  34146  pclfinN  34204  ldilcnv  34419  ldilco  34420  cdleme25dN  34662  cdlemj2  35128  tendocan  35130  erng1lem  35293  erngdvlem4-rN  35305  dihord2pre  35532  dihglblem2N  35601  dochvalr  35664  hdmap14lem12  36189  hdmap14lem13  36190  pellfundre  36463  pellfundge  36464  pellfundlb  36466  dford3lem1  36611  aomclem2  36643  pwinfi3  36887  iunrelexp0  37013  iunrelexpmin1  37019  iunrelexpmin2  37023  dftrcl3  37031  cnvtrclfv  37035  trclimalb2  37037  dfrtrcl3  37044  ntrneiel2  37404  ntrneik4w  37418  ntrrn  37440  gneispa  37448  gneispb  37449  addrcom  37700  iunconlem2  38193  ssuzfz  38506  dvmptfprod  38835  dvnprodlem3  38838  funressnfv  39857  tz6.12-afv  39902  iccpartltu  39963  iccpartgtl  39964  iccpartleu  39966  iccpartgel  39967  bgoldbst  40200  bgoldbtbnd  40225  tgblthelfgott  40229  tgblthelfgottOLD  40236  otiunsndisjX  40317  nbuhgr  40565  nbumgr  40569  uhgrnbgr0nb  40576  uvtxanbgrvtx  40619  cusgrfilem2  40672  uspgr2wlkeq  40854  wwlks  41038  2wspiundisj  41166  rusgr0edg  41176  clwwisshclwwslem  41234  3cyclfrgrrn  41456  vdgn1frgrv3  41467  av-numclwlk2lem2f1o  41535  av-frgraregord013  41549  nnsgrp  41607  ellcoellss  42018  lindsrng01  42051  suppdm  42094  nn0sumshdiglem1  42213  ssdifsn  42228  setrec2fun  42238
  Copyright terms: Public domain W3C validator