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

Theorem ralrimiv 2994
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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 2983 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-ral 2946
This theorem is referenced by:  ralrimiva  2995  ralrimivw  2996  ralrimdv  2997  ralrimivv  2999  reximdvai  3044  r19.27v  3099  raleleq  3186  rr19.3v  3377  rabssdv  3715  rzal  4106  ssdifsn  4351  disjord  4673  disjiund  4675  trin  4796  class2seteq  4863  ralxfrALT  4917  otiunsndisj  5009  issref  5544  onmindif  5853  fnprb  6513  fntpb  6514  ssorduni  7027  onminex  7049  onmindif2  7054  suceloni  7055  limuni3  7094  frxp  7332  poxp  7334  wfrlem15  7474  onfununi  7483  onnseq  7486  tfrlem12  7530  tz7.48-2  7582  oaass  7686  omass  7705  oelim2  7720  oelimcl  7725  oaabs2  7770  omabs  7772  undifixp  7986  dom2lem  8037  isinf  8214  unblem4  8256  unbnn2  8258  marypha1lem  8380  supiso  8422  ordiso2  8461  card2inf  8501  elirrv  8542  wemapwe  8632  trcl  8642  tz9.13  8692  rankval3b  8727  rankunb  8751  rankuni2b  8754  scott0  8787  dfac8alem  8890  carduniima  8957  alephsmo  8963  alephval3  8971  iunfictbso  8975  dfac3  8982  dfac5lem5  8988  dfac12r  9006  dfac12k  9007  kmlem4  9013  kmlem11  9020  cfsuc  9117  cofsmo  9129  cfsmolem  9130  coftr  9133  alephsing  9136  infpssrlem3  9165  fin23lem30  9202  isf32lem2  9214  isf32lem3  9215  isf34lem6  9240  fin1a2lem11  9270  fin1a2lem13  9272  fin1a2s  9274  axcc2lem  9296  domtriomlem  9302  axdc3lem2  9311  axdc4lem  9315  axcclem  9317  axdclem2  9380  iundom2g  9400  uniimadom  9404  cardmin  9424  alephval2  9432  alephreg  9442  fpwwe2lem12  9501  wunex2  9598  wuncval2  9607  tskwe2  9633  inar1  9635  tskuni  9643  gruun  9666  intgru  9674  grutsk1  9681  genpcl  9868  ltexprlem5  9900  suplem1pr  9912  supexpr  9914  supsrlem  9970  axpre-sup  10028  fiminre  11010  supaddc  11028  supadd  11029  supmul1  11030  supmullem1  11031  supmul  11033  peano5nni  11061  uzind  11507  zindd  11516  uzwo  11789  lbzbi  11814  xrsupsslem  12175  xrinfmsslem  12176  supxrun  12184  supxrpnf  12186  supxrunb1  12187  supxrunb2  12188  icoshftf1o  12333  flval3  12656  axdc4uzlem  12822  ccatrn  13407  2cshw  13605  cshweqrep  13613  s3iunsndisj  13753  rtrclreclem4  13845  dfrtrcl2  13846  sqrlem1  14027  sqrlem6  14032  fsum0diag2  14559  alzdvds  15089  gcdcllem1  15268  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  maxprmfct  15468  hashgcdeq  15541  unbenlem  15659  vdwlem6  15737  vdwlem10  15741  firest  16140  mrieqv2d  16346  iscatd  16381  setcmon  16784  setcepi  16785  fullestrcsetc  16838  fullsetcestrc  16853  isglbd  17164  isacs4lem  17215  acsfiindd  17224  acsmapd  17225  psss  17261  ghmrn  17720  ghmpreima  17729  cntz2ss  17811  symgextres  17891  psgnunilem2  17961  lsmsubg  18115  efgsfo  18198  gsumzaddlem  18367  gsummptnn0fzfv  18430  dmdprdd  18444  dprd2da  18487  imasring  18665  isabvd  18868  issrngd  18909  islssd  18984  lbsextlem3  19208  lbsextlem4  19209  lidldvgen  19303  psgnghm  19974  isphld  20047  frlmsslsp  20183  mp2pm2mplem4  20662  tgcl  20821  distop  20847  indistopon  20853  pptbas  20860  toponmre  20945  opnnei  20972  neiuni  20974  neindisj2  20975  ordtrest2  21056  cnpnei  21116  cnindis  21144  cmpcld  21253  uncmp  21254  hauscmplem  21257  2ndc1stc  21302  1stcrest  21304  1stcelcls  21312  llyrest  21336  nllyrest  21337  cldllycmp  21346  reftr  21365  locfincf  21382  comppfsc  21383  txcls  21455  ptpjcn  21462  ptclsg  21466  dfac14lem  21468  xkoccn  21470  txlly  21487  txnlly  21488  ptrescn  21490  tx1stc  21501  xkoco1cn  21508  xkoco2cn  21509  xkococn  21511  xkoinjcn  21538  qtopeu  21567  hmeofval  21609  ordthmeolem  21652  isfild  21709  fbasrn  21735  trfil2  21738  flimclslem  21835  fclsrest  21875  fclscf  21876  flimfcls  21877  alexsubALTlem1  21898  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALT  21902  qustgpopn  21970  isxmetd  22178  imasdsf1olem  22225  blcls  22358  prdsxmslem2  22381  metustfbas  22409  dscmet  22424  nrmmetd  22426  reperflem  22668  reconnlem2  22677  xrge0tsms  22684  fsumcn  22720  cnheibor  22801  tchcph  23082  lmmbr  23102  caubl  23152  ivthlem1  23266  ovolctb  23304  ovoliunlem2  23317  ovolscalem1  23327  ovolicc2  23336  voliunlem3  23366  ismbfd  23452  mbfimaopnlem  23467  itg2le  23551  ellimc2  23686  c1liplem1  23804  plyeq0lem  24011  dgreq0  24066  aannenlem1  24128  pilem2  24251  cxpcn3lem  24533  scvxcvx  24757  musum  24962  dchrisum0flb  25244  ostth2lem2  25368  numedglnl  26084  upgrreslem  26241  umgrreslem  26242  nbuhgr  26284  nbumgr  26288  uhgrnbgr0nb  26295  uvtxnbgrvtx  26341  cusgrfilem2  26408  uspgr2wlkeq  26598  wwlks  26783  iswwlksnon  26802  rusgr0edg  26940  clwwisshclwwslem  26971  clwwlkn  26985  clwwlknon  27063  3cyclfrgrrn  27266  vdgn1frgrv3  27277  2wspmdisj  27317  clwwlkccatlem  27331  numclwlk2lem2f1o  27359  numclwlk2lem2f1oOLD  27366  frgrregord013  27382  htthlem  27902  ocsh  28270  shintcli  28316  pjss2coi  29151  pjnormssi  29155  pjclem4  29186  pj3si  29194  pj3cor1i  29196  strlem3a  29239  strb  29245  hstrlem3a  29247  hstrbi  29253  spansncv2  29280  mdsl1i  29308  cvmdi  29311  mdexchi  29322  h1da  29336  mdsymlem6  29395  sumdmdii  29402  dmdbr5ati  29409  isoun  29607  supssd  29615  infssd  29616  xrge0tsmsd  29913  ordtrest2NEW  30097  pwsiga  30321  measiun  30409  dya2iocuni  30473  bnj518  31082  bnj1137  31189  bnj1136  31191  bnj1413  31229  bnj1417  31235  bnj60  31256  erdszelem8  31306  cvmsss2  31382  cvmfolem  31387  dfon2lem8  31819  dfon2lem9  31820  dfon2  31821  rdgprc  31824  trpredtr  31854  trpredmintr  31855  trpredelss  31856  dftrpred3g  31857  trpredpo  31859  trpredrec  31862  frr3g  31904  frrlem5b  31910  frrlem5d  31912  sltval2  31934  nolesgn2ores  31950  nosupres  31978  nosupbnd2lem1  31986  scutun12  32042  nn0prpwlem  32442  ntruni  32447  clsint2  32449  fneint  32468  fnessref  32477  refssfne  32478  neibastop1  32479  neibastop2lem  32480  bj-0int  33180  bj-ismooredr2  33190  relowlpssretop  33342  heicant  33574  mblfinlem1  33576  ftc2nc  33624  sdclem2  33668  fdc  33671  seqpo  33673  prdsbnd  33722  heibor  33750  rrnequiv  33764  0idl  33954  intidl  33958  unichnidl  33960  prnc  33996  uniqsALTV  34242  lsmcv2  34634  lcvexchlem4  34642  lcvexchlem5  34643  eqlkr  34704  paddclN  35446  pclfinN  35504  ldilcnv  35719  ldilco  35720  cdleme25dN  35961  cdlemj2  36427  tendocan  36429  erng1lem  36592  erngdvlem4-rN  36604  dihord2pre  36831  dihglblem2N  36900  dochvalr  36963  hdmap14lem12  37488  hdmap14lem13  37489  pellfundre  37762  pellfundge  37763  pellfundlb  37765  dford3lem1  37910  aomclem2  37942  pwinfi3  38185  iunrelexp0  38311  iunrelexpmin1  38317  iunrelexpmin2  38321  dftrcl3  38329  cnvtrclfv  38333  trclimalb2  38335  dfrtrcl3  38342  ntrneiel2  38701  ntrneik4w  38715  ntrrn  38737  gneispa  38745  gneispb  38746  addrcom  38996  iunconnlem2  39485  ssuzfz  39878  dvmptfprod  40478  dvnprodlem3  40481  funressnfv  41529  tz6.12-afv  41574  otiunsndisjX  41621  iccpartltu  41686  iccpartgtl  41687  iccpartleu  41689  iccpartgel  41690  fargshiftf  41701  fargshiftfva  41704  sbgoldbst  41991  bgoldbtbnd  42022  tgblthelfgott  42028  tgblthelfgottOLD  42034  nnsgrp  42142  ellcoellss  42549  lindsrng01  42582  suppdm  42625  nn0sumshdiglem1  42740  setrec2fun  42764
  Copyright terms: Public domain W3C validator