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

Theorem ralrimiv 3143
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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 3142 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ral 3066
This theorem is referenced by:  ralrimiva  3144  ralrimivw  3148  ralrimdv  3150  reximdvaiOLD  3164  ralrimivv  3196  raleleq  3320  rr19.3v  3624  class2seteq  3667  rabssdv  4037  rzalALT  4472  disjord  5098  disjiund  5100  trin  5239  ralxfrALT  5375  otiunsndisj  5482  onmindif  6414  fnprb  7163  fntpb  7164  f1cdmsn  7233  ssorduni  7718  onminex  7742  onmindif2  7747  sucexeloniOLD  7750  suceloniOLD  7752  limuni3  7793  frxp  8063  poxp  8065  sexp2  8083  sexp3  8090  wfrlem15OLD  8274  onfununi  8292  onnseq  8295  tfrlem12  8340  tz7.48-2  8393  oaass  8513  omass  8532  oelim2  8547  oelimcl  8552  oaabs2  8600  omabs  8602  undifixp  8879  dom2lem  8939  isinf  9211  isinfOLD  9212  unblem4  9249  unbnn2  9251  marypha1lem  9376  supiso  9418  ordiso2  9458  card2inf  9498  elirrv  9539  wemapwe  9640  ttrclss  9663  trcl  9671  frr3g  9699  tz9.13  9734  rankval3b  9769  rankunb  9793  rankuni2b  9796  scott0  9829  updjud  9877  dfac8alem  9972  carduniima  10039  alephsmo  10045  alephval3  10053  iunfictbso  10057  dfac3  10064  dfac5lem5  10070  dfac12r  10089  dfac12k  10090  kmlem4  10096  kmlem11  10103  cfsuc  10200  cofsmo  10212  cfsmolem  10213  coftr  10216  alephsing  10219  infpssrlem3  10248  fin23lem30  10285  isf32lem2  10297  isf32lem3  10298  isf34lem6  10323  fin1a2lem11  10353  fin1a2lem13  10355  fin1a2s  10357  axcc2lem  10379  domtriomlem  10385  axdc3lem2  10394  axdc4lem  10398  axcclem  10400  axdclem2  10463  iundom2g  10483  uniimadom  10487  cardmin  10507  alephval2  10515  alephreg  10525  fpwwe2lem11  10584  wunex2  10681  wuncval2  10690  tskwe2  10716  inar1  10718  tskuni  10726  gruun  10749  intgru  10757  grutsk1  10764  genpcl  10951  ltexprlem5  10983  suplem1pr  10995  supexpr  10997  supsrlem  11054  axpre-sup  11112  negfi  12111  supaddc  12129  supadd  12130  supmul1  12131  supmullem1  12132  supmul  12134  peano5nni  12163  uzind  12602  zindd  12611  uzwo  12843  lbzbi  12868  xrsupsslem  13233  xrinfmsslem  13234  supxrun  13242  supxrpnf  13244  supxrunb1  13245  supxrunb2  13246  icoshftf1o  13398  flval3  13727  axdc4uzlem  13895  wrdnfi  14443  ccatrn  14484  ccatalpha  14488  2cshw  14708  cshweqrep  14716  s3iunsndisj  14860  rtrclreclem4  14953  dfrtrcl2  14954  01sqrexlem1  15134  01sqrexlem6  15139  fsum0diag2  15675  alzdvds  16209  gcdcllem1  16386  lcmfunsnlem2lem1  16521  lcmfunsnlem2lem2  16522  maxprmfct  16592  hashgcdeq  16668  unbenlem  16787  vdwlem6  16865  vdwlem10  16869  firest  17321  mrieqv2d  17526  iscatd  17560  initoeu2  17909  setcmon  17980  setcepi  17981  fullestrcsetc  18046  fullsetcestrc  18061  isglbd  18405  isacs4lem  18440  acsfiindd  18449  acsmapd  18450  psss  18476  sgrpidmnd  18568  pwmnd  18754  ghmrn  19028  ghmpreima  19037  cntz2ss  19120  symgextres  19214  psgnunilem2  19284  lsmsubg  19443  efgsfo  19528  gsumzaddlem  19705  gsummptnn0fzfv  19771  dmdprdd  19785  dprd2da  19828  ablsimpgprmd  19901  imasring  20052  isabvd  20295  issrngd  20336  islssd  20412  lbsextlem3  20637  lbsextlem4  20638  lidldvgen  20741  psgnghm  21000  isphld  21074  frlmsslsp  21218  mp2pm2mplem4  22174  tgcl  22335  distop  22361  indistopon  22367  pptbas  22374  toponmre  22460  opnnei  22487  neiuni  22489  neindisj2  22490  ordtrest2  22571  cnpnei  22631  cnindis  22659  cmpcld  22769  uncmp  22770  hauscmplem  22773  2ndc1stc  22818  1stcrest  22820  1stcelcls  22828  llyrest  22852  nllyrest  22853  cldllycmp  22862  reftr  22881  locfincf  22898  comppfsc  22899  txcls  22971  ptpjcn  22978  ptclsg  22982  dfac14lem  22984  xkoccn  22986  txlly  23003  txnlly  23004  ptrescn  23006  tx1stc  23017  xkoco1cn  23024  xkoco2cn  23025  xkococn  23027  xkoinjcn  23054  qtopeu  23083  hmeofval  23125  ordthmeolem  23168  isfild  23225  fbasrn  23251  trfil2  23254  flimclslem  23351  fclsrest  23391  fclscf  23392  flimfcls  23393  alexsubALTlem1  23414  alexsubALTlem2  23415  alexsubALTlem3  23416  alexsubALT  23418  qustgpopn  23487  isxmetd  23695  imasdsf1olem  23742  blcls  23878  prdsxmslem2  23901  metustfbas  23929  dscmet  23944  nrmmetd  23946  reperflem  24197  reconnlem2  24206  xrge0tsms  24213  fsumcn  24249  cnheibor  24334  tcphcph  24617  lmmbr  24638  caubl  24688  ivthlem1  24831  ovolctb  24870  ovoliunlem2  24883  ovolscalem1  24893  ovolicc2  24902  voliunlem3  24932  ismbfd  25019  mbfimaopnlem  25035  itg2le  25120  ellimc2  25257  c1liplem1  25376  plyeq0lem  25587  dgreq0  25642  aannenlem1  25704  pilem2  25827  cxpcn3lem  26116  scvxcvx  26351  musum  26556  dchrisum0flb  26874  ostth2lem2  26998  sltval2  27020  nolesgn2ores  27036  nogesgn1ores  27038  nosupres  27071  nosupbnd2lem1  27079  noinfres  27086  noinfbnd2lem1  27094  scutun12  27171  madebdayim  27239  numedglnl  28137  upgrreslem  28294  umgrreslem  28295  nbuhgr  28333  nbumgr  28337  uhgrnbgr0nb  28344  nbusgrf1o0  28359  uvtxnbgrvtx  28383  cusgrfilem2  28446  uspgr2wlkeq  28636  wwlks  28822  iswwlksnon  28840  rusgr0edg  28960  clwwlkccatlem  28975  clwwisshclwwslem  29000  clwwlkn  29012  clwwlknon  29076  3cyclfrgrrn  29272  vdgn1frgrv3  29283  2wspmdisj  29323  numclwlk2lem2f1o  29365  frgrregord013  29381  htthlem  29901  ocsh  30267  shintcli  30313  pjss2coi  31148  pjnormssi  31152  pjclem4  31183  pj3si  31191  pj3cor1i  31193  strlem3a  31236  strb  31242  hstrlem3a  31244  hstrbi  31250  spansncv2  31277  mdsl1i  31305  cvmdi  31308  mdexchi  31319  h1da  31333  mdsymlem6  31392  sumdmdii  31399  dmdbr5ati  31406  isoun  31657  supssd  31668  infssd  31669  xrge0tsmsd  31941  ordtrest2NEW  32544  pwsiga  32769  measiun  32857  dya2iocuni  32923  bnj518  33538  bnj1137  33647  bnj1136  33649  bnj1413  33687  bnj1417  33693  bnj60  33714  subgrwlk  33766  erdszelem8  33832  cvmsss2  33908  cvmfolem  33913  fmlasucdisj  34033  satfun  34045  dfon2lem8  34404  dfon2lem9  34405  dfon2  34406  rdgprc  34408  nn0prpwlem  34823  ntruni  34828  clsint2  34830  fneint  34849  fnessref  34858  refssfne  34859  neibastop1  34860  neibastop2lem  34861  bj-0int  35601  bj-ismooredr  35609  relowlpssretop  35864  fvineqsneu  35911  fvineqsneq  35912  heicant  36142  mblfinlem1  36144  ftc2nc  36189  sdclem2  36230  fdc  36233  seqpo  36235  prdsbnd  36281  heibor  36309  rrnequiv  36323  0idl  36513  intidl  36517  unichnidl  36519  prnc  36555  uniqsALTV  36819  refressn  36934  lsmcv2  37520  lcvexchlem4  37528  lcvexchlem5  37529  eqlkr  37590  paddclN  38334  pclfinN  38392  ldilcnv  38607  ldilco  38608  cdleme25dN  38848  cdlemj2  39314  tendocan  39316  erng1lem  39479  erngdvlem4-rN  39491  dihord2pre  39717  dihglblem2N  39786  dochvalr  39849  hdmap14lem12  40371  hdmap14lem13  40372  fsuppind  40794  pellfundre  41233  pellfundge  41234  pellfundlb  41236  dford3lem1  41379  aomclem2  41411  oaabsb  41658  cantnf2  41689  ofoafg  41699  naddcnff  41707  naddwordnexlem3  41745  naddwordnexlem4  41747  pwinfi3  41909  iunrelexp0  42048  iunrelexpmin1  42054  iunrelexpmin2  42058  dftrcl3  42066  cnvtrclfv  42070  trclimalb2  42072  dfrtrcl3  42079  ntrneiel2  42432  ntrneik4w  42446  ntrrn  42468  gneispa  42476  gneispb  42477  addrcom  42829  iunconnlem2  43291  ssuzfz  43657  dvmptfprod  44260  dvnprodlem3  44263  funressnfv  45351  cfsetsnfsetfo  45368  tz6.12-afv  45479  tz6.12-afv2  45546  otiunsndisjX  45585  uniimaprimaeqfv  45648  iccpartltu  45691  iccpartgtl  45692  iccpartleu  45694  iccpartgel  45695  fargshiftf  45706  fargshiftfva  45709  sbgoldbst  46044  bgoldbtbnd  46075  tgblthelfgott  46081  isomushgr  46092  nnsgrp  46185  ellcoellss  46590  lindsrng01  46623  suppdm  46665  nn0sumshdiglem1  46781  setrec2fun  47211
  Copyright terms: Public domain W3C validator