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

Theorem ralrimiv 2947
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 1826 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 2936 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-ral 2900
This theorem is referenced by:  ralrimiva  2948  ralrimivw  2949  ralrimdv  2950  ralrimivv  2952  reximdvai  2997  r19.27v  3051  raleleq  3132  rr19.3v  3313  rabssdv  3644  rzal  4024  trin  4685  class2seteq  4753  ralxfrALT  4807  otiunsndisj  4895  issref  5414  onmindif  5717  fnprb  6354  fntpb  6355  ssorduni  6854  onminex  6876  onmindif2  6881  suceloni  6882  limuni3  6921  frxp  7151  poxp  7153  wfrlem15  7293  onfununi  7302  onnseq  7305  tfrlem12  7349  tz7.48-2  7401  oaass  7505  omass  7524  oelim2  7539  oelimcl  7544  oaabs2  7589  omabs  7591  undifixp  7807  dom2lem  7858  isinf  8035  unblem4  8077  unbnn2  8079  marypha1lem  8199  supiso  8241  ordiso2  8280  card2inf  8320  elirrv  8364  wemapwe  8454  trcl  8464  tz9.13  8514  rankval3b  8549  rankunb  8573  rankuni2b  8576  scott0  8609  dfac8alem  8712  carduniima  8779  alephsmo  8785  alephval3  8793  iunfictbso  8797  dfac3  8804  dfac5lem5  8810  dfac12r  8828  dfac12k  8829  kmlem4  8835  kmlem11  8842  cfsuc  8939  cofsmo  8951  cfsmolem  8952  coftr  8955  alephsing  8958  infpssrlem3  8987  fin23lem30  9024  isf32lem2  9036  isf32lem3  9037  isf34lem6  9062  fin1a2lem11  9092  fin1a2lem13  9094  fin1a2s  9096  axcc2lem  9118  domtriomlem  9124  axdc3lem2  9133  axdc4lem  9137  axcclem  9139  axdclem2  9202  iundom2g  9218  uniimadom  9222  cardmin  9242  alephval2  9250  alephreg  9260  fpwwe2lem12  9319  wunex2  9416  wuncval2  9425  tskwe2  9451  inar1  9453  tskuni  9461  gruun  9484  intgru  9492  grutsk1  9499  genpcl  9686  ltexprlem5  9718  suplem1pr  9730  supexpr  9732  supsrlem  9788  axpre-sup  9846  fiminre  10823  supaddc  10839  supadd  10840  supmul1  10841  supmullem1  10842  supmul  10844  peano5nni  10872  uzind  11303  zindd  11312  uzwo  11585  lbzbi  11610  xrsupsslem  11967  xrinfmsslem  11968  supxrun  11976  supxrpnf  11978  supxrunb1  11979  supxrunb2  11980  icoshftf1o  12124  flval3  12435  axdc4uzlem  12601  ccatrn  13173  2cshw  13358  cshweqrep  13366  s3iunsndisj  13503  rtrclreclem4  13597  dfrtrcl2  13598  sqrlem1  13779  sqrlem6  13784  fsum0diag2  14305  alzdvds  14828  gcdcllem1  15007  lcmfunsnlem2lem1  15137  lcmfunsnlem2lem2  15138  maxprmfct  15207  hashgcdeq  15280  unbenlem  15398  vdwlem6  15476  vdwlem10  15480  firest  15864  mrieqv2d  16070  iscatd  16105  setcmon  16508  setcepi  16509  fullestrcsetc  16562  fullsetcestrc  16577  isglbd  16888  isacs4lem  16939  acsfiindd  16948  acsmapd  16949  psss  16985  ghmrn  17444  ghmpreima  17453  cntz2ss  17536  symgextres  17616  psgnunilem2  17686  lsmsubg  17840  efgsfo  17923  gsumzaddlem  18092  gsummptnn0fzfv  18155  dmdprdd  18169  dprd2da  18212  imasring  18390  isabvd  18591  issrngd  18632  islssd  18705  lbsextlem3  18929  lbsextlem4  18930  lidldvgen  19024  psgnghm  19692  isphld  19765  frlmsslsp  19901  mp2pm2mplem4  20380  tgcl  20531  distop  20557  indistopon  20562  pptbas  20569  toponmre  20654  opnnei  20681  neiuni  20683  neindisj2  20684  ordtrest2  20765  cnpnei  20825  cnindis  20853  cmpcld  20962  uncmp  20963  hauscmplem  20966  2ndc1stc  21011  1stcrest  21013  1stcelcls  21021  llyrest  21045  nllyrest  21046  cldllycmp  21055  reftr  21074  locfincf  21091  comppfsc  21092  txcls  21164  ptpjcn  21171  ptclsg  21175  dfac14lem  21177  xkoccn  21179  txlly  21196  txnlly  21197  ptrescn  21199  tx1stc  21210  xkoco1cn  21217  xkoco2cn  21218  xkococn  21220  xkoinjcn  21247  qtopeu  21276  hmeofval  21318  ordthmeolem  21361  isfild  21419  fbasrn  21445  trfil2  21448  flimclslem  21545  fclsrest  21585  fclscf  21586  flimfcls  21587  alexsubALTlem1  21608  alexsubALTlem2  21609  alexsubALTlem3  21610  alexsubALT  21612  qustgpopn  21680  isxmetd  21888  imasdsf1olem  21935  blcls  22068  prdsxmslem2  22091  metustfbas  22119  dscmet  22134  nrmmetd  22136  reperflem  22376  reconnlem2  22385  xrge0tsms  22392  fsumcn  22428  cnheibor  22509  tchcph  22788  lmmbr  22808  caubl  22858  ivthlem1  22971  ovolctb  23009  ovoliunlem2  23022  ovolscalem1  23032  ovolicc2  23041  voliunlem3  23071  ismbfd  23157  mbfimaopnlem  23172  itg2le  23256  ellimc2  23391  c1liplem1  23507  plyeq0lem  23714  dgreq0  23769  aannenlem1  23831  pilem2  23954  cxpcn3lem  24232  scvxcvx  24456  musum  24661  dchrisum0flb  24943  ostth2lem2  25067  usgrares1  25732  nbusgra  25750  nbgra0nb  25751  nbgra0edg  25754  cusgrafilem2  25801  usgrasscusgra  25804  uvtxnbgravtx  25816  fargshiftf  25957  fargshiftfva  25960  usg2wlkeq  26029  clwwlkn0  26095  clwwisshclwwlem  26127  0egra0rgra  26256  eupatrl  26288  eupap1  26296  3cyclfrgrarn  26333  vdgn1frgrav3  26348  2spotiundisj  26382  numclwlk2lem2f1o  26425  frgraregord013  26438  htthlem  26951  ocsh  27319  shintcli  27365  pjss2coi  28200  pjnormssi  28204  pjclem4  28235  pj3si  28243  pj3cor1i  28245  strlem3a  28288  strb  28294  hstrlem3a  28296  hstrbi  28302  spansncv2  28329  mdsl1i  28357  cvmdi  28360  mdexchi  28371  h1da  28385  mdsymlem6  28444  sumdmdii  28451  dmdbr5ati  28458  isoun  28655  supssd  28663  infssd  28664  xrge0tsmsd  28909  ordtrest2NEW  29090  pwsiga  29313  measiun  29401  dya2iocuni  29465  bnj518  30003  bnj1137  30110  bnj1136  30112  bnj1413  30150  bnj1417  30156  bnj60  30177  erdszelem8  30227  cvmsss2  30303  cvmfolem  30308  dfon2lem8  30732  dfon2lem9  30733  dfon2  30734  rdgprc  30737  trpredtr  30767  trpredmintr  30768  trpredelss  30769  dftrpred3g  30770  trpredpo  30772  trpredrec  30775  frr3g  30816  frrlem5b  30822  frrlem5d  30824  sltval2  30846  nn0prpwlem  31280  ntruni  31285  clsint2  31287  fneint  31306  fnessref  31315  refssfne  31316  neibastop1  31317  neibastop2lem  31318  relowlpssretop  32171  heicant  32397  mblfinlem1  32399  ftc2nc  32447  sdclem2  32491  fdc  32494  seqpo  32496  prdsbnd  32545  heibor  32573  rrnequiv  32587  0idl  32777  intidl  32781  unichnidl  32783  prnc  32819  lsmcv2  33117  lcvexchlem4  33125  lcvexchlem5  33126  eqlkr  33187  paddclN  33929  pclfinN  33987  ldilcnv  34202  ldilco  34203  cdleme25dN  34445  cdlemj2  34911  tendocan  34913  erng1lem  35076  erngdvlem4-rN  35088  dihord2pre  35315  dihglblem2N  35384  dochvalr  35447  hdmap14lem12  35972  hdmap14lem13  35973  pellfundre  36246  pellfundge  36247  pellfundlb  36249  dford3lem1  36394  aomclem2  36426  pwinfi3  36670  iunrelexp0  36796  iunrelexpmin1  36802  iunrelexpmin2  36806  dftrcl3  36814  cnvtrclfv  36818  trclimalb2  36820  dfrtrcl3  36827  ntrneiel2  37187  ntrneik4w  37201  ntrrn  37223  gneispa  37231  gneispb  37232  addrcom  37483  iunconlem2  37976  ssuzfz  38289  dvmptfprod  38618  dvnprodlem3  38621  funressnfv  39640  tz6.12-afv  39686  iccpartltu  39747  iccpartgtl  39748  iccpartleu  39750  iccpartgel  39751  bgoldbst  39984  bgoldbtbnd  40009  tgblthelfgott  40013  tgblthelfgottOLD  40020  otiunsndisjX  40111  nbuhgr  40546  nbumgr  40550  uhgrnbgr0nb  40557  uvtxanbgrvtx  40600  cusgrfilem2  40653  uspgr2wlkeq  40835  wwlks  41019  2wspiundisj  41147  rusgr0edg  41157  clwwisshclwwslem  41215  3cyclfrgrrn  41437  vdgn1frgrv3  41448  av-numclwlk2lem2f1o  41516  av-frgraregord013  41530  nnsgrp  41588  ellcoellss  41999  lindsrng01  42032  suppdm  42075  nn0sumshdiglem1  42194
  Copyright terms: Public domain W3C validator