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

Theorem ralrimiv 3103
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 1988 . 2 (𝜑 → ∀𝑥𝜑)
2 ralrimiv.1 . 2 (𝜑 → (𝑥𝐴𝜓))
31, 2hbralrimi 3092 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-ral 3055
This theorem is referenced by:  ralrimiva  3104  ralrimivw  3105  ralrimdv  3106  ralrimivv  3108  reximdvai  3153  r19.27v  3208  raleleq  3295  rr19.3v  3485  rabssdv  3823  rzal  4217  ssdifsnOLD  4464  disjord  4793  disjiund  4795  trin  4915  class2seteq  4982  ralxfrALT  5036  otiunsndisj  5130  issref  5667  onmindif  5976  fnprb  6636  fntpb  6637  ssorduni  7150  onminex  7172  onmindif2  7177  suceloni  7178  limuni3  7217  frxp  7455  poxp  7457  wfrlem15  7598  onfununi  7607  onnseq  7610  tfrlem12  7654  tz7.48-2  7706  oaass  7810  omass  7829  oelim2  7844  oelimcl  7849  oaabs2  7894  omabs  7896  undifixp  8110  dom2lem  8161  isinf  8338  unblem4  8380  unbnn2  8382  marypha1lem  8504  supiso  8546  ordiso2  8585  card2inf  8625  elirrv  8666  wemapwe  8767  trcl  8777  tz9.13  8827  rankval3b  8862  rankunb  8886  rankuni2b  8889  scott0  8922  dfac8alem  9042  carduniima  9109  alephsmo  9115  alephval3  9123  iunfictbso  9127  dfac3  9134  dfac5lem5  9140  dfac12r  9160  dfac12k  9161  kmlem4  9167  kmlem11  9174  cfsuc  9271  cofsmo  9283  cfsmolem  9284  coftr  9287  alephsing  9290  infpssrlem3  9319  fin23lem30  9356  isf32lem2  9368  isf32lem3  9369  isf34lem6  9394  fin1a2lem11  9424  fin1a2lem13  9426  fin1a2s  9428  axcc2lem  9450  domtriomlem  9456  axdc3lem2  9465  axdc4lem  9469  axcclem  9471  axdclem2  9534  iundom2g  9554  uniimadom  9558  cardmin  9578  alephval2  9586  alephreg  9596  fpwwe2lem12  9655  wunex2  9752  wuncval2  9761  tskwe2  9787  inar1  9789  tskuni  9797  gruun  9820  intgru  9828  grutsk1  9835  genpcl  10022  ltexprlem5  10054  suplem1pr  10066  supexpr  10068  supsrlem  10124  axpre-sup  10182  fiminre  11164  supaddc  11182  supadd  11183  supmul1  11184  supmullem1  11185  supmul  11187  peano5nni  11215  uzind  11661  zindd  11670  uzwo  11944  lbzbi  11969  xrsupsslem  12330  xrinfmsslem  12331  supxrun  12339  supxrpnf  12341  supxrunb1  12342  supxrunb2  12343  icoshftf1o  12488  flval3  12810  axdc4uzlem  12976  ccatrn  13561  2cshw  13759  cshweqrep  13767  s3iunsndisj  13908  rtrclreclem4  14000  dfrtrcl2  14001  sqrlem1  14182  sqrlem6  14187  fsum0diag2  14714  alzdvds  15244  gcdcllem1  15423  lcmfunsnlem2lem1  15553  lcmfunsnlem2lem2  15554  maxprmfct  15623  hashgcdeq  15696  unbenlem  15814  vdwlem6  15892  vdwlem10  15896  firest  16295  mrieqv2d  16501  iscatd  16535  setcmon  16938  setcepi  16939  fullestrcsetc  16992  fullsetcestrc  17007  isglbd  17318  isacs4lem  17369  acsfiindd  17378  acsmapd  17379  psss  17415  ghmrn  17874  ghmpreima  17883  cntz2ss  17965  symgextres  18045  psgnunilem2  18115  lsmsubg  18269  efgsfo  18352  gsumzaddlem  18521  gsummptnn0fzfv  18584  dmdprdd  18598  dprd2da  18641  imasring  18819  isabvd  19022  issrngd  19063  islssd  19138  lbsextlem3  19362  lbsextlem4  19363  lidldvgen  19457  psgnghm  20128  isphld  20201  frlmsslsp  20337  mp2pm2mplem4  20816  tgcl  20975  distop  21001  indistopon  21007  pptbas  21014  toponmre  21099  opnnei  21126  neiuni  21128  neindisj2  21129  ordtrest2  21210  cnpnei  21270  cnindis  21298  cmpcld  21407  uncmp  21408  hauscmplem  21411  2ndc1stc  21456  1stcrest  21458  1stcelcls  21466  llyrest  21490  nllyrest  21491  cldllycmp  21500  reftr  21519  locfincf  21536  comppfsc  21537  txcls  21609  ptpjcn  21616  ptclsg  21620  dfac14lem  21622  xkoccn  21624  txlly  21641  txnlly  21642  ptrescn  21644  tx1stc  21655  xkoco1cn  21662  xkoco2cn  21663  xkococn  21665  xkoinjcn  21692  qtopeu  21721  hmeofval  21763  ordthmeolem  21806  isfild  21863  fbasrn  21889  trfil2  21892  flimclslem  21989  fclsrest  22029  fclscf  22030  flimfcls  22031  alexsubALTlem1  22052  alexsubALTlem2  22053  alexsubALTlem3  22054  alexsubALT  22056  qustgpopn  22124  isxmetd  22332  imasdsf1olem  22379  blcls  22512  prdsxmslem2  22535  metustfbas  22563  dscmet  22578  nrmmetd  22580  reperflem  22822  reconnlem2  22831  xrge0tsms  22838  fsumcn  22874  cnheibor  22955  tchcph  23236  lmmbr  23256  caubl  23306  ivthlem1  23420  ovolctb  23458  ovoliunlem2  23471  ovolscalem1  23481  ovolicc2  23490  voliunlem3  23520  ismbfd  23606  mbfimaopnlem  23621  itg2le  23705  ellimc2  23840  c1liplem1  23958  plyeq0lem  24165  dgreq0  24220  aannenlem1  24282  pilem2  24405  cxpcn3lem  24687  scvxcvx  24911  musum  25116  dchrisum0flb  25398  ostth2lem2  25522  numedglnl  26238  upgrreslem  26395  umgrreslem  26396  nbuhgr  26438  nbumgr  26442  uhgrnbgr0nb  26449  uvtxnbgrvtx  26495  cusgrfilem2  26562  uspgr2wlkeq  26752  wwlks  26938  iswwlksnon  26957  rusgr0edg  27095  clwwlkccatlem  27112  clwwisshclwwslem  27137  clwwlkn  27151  clwwlknon  27235  3cyclfrgrrn  27440  vdgn1frgrv3  27451  2wspmdisj  27491  numclwlk2lem2f1o  27540  numclwlk2lem2f1oOLD  27547  frgrregord013  27563  htthlem  28083  ocsh  28451  shintcli  28497  pjss2coi  29332  pjnormssi  29336  pjclem4  29367  pj3si  29375  pj3cor1i  29377  strlem3a  29420  strb  29426  hstrlem3a  29428  hstrbi  29434  spansncv2  29461  mdsl1i  29489  cvmdi  29492  mdexchi  29503  h1da  29517  mdsymlem6  29576  sumdmdii  29583  dmdbr5ati  29590  isoun  29788  supssd  29796  infssd  29797  xrge0tsmsd  30094  ordtrest2NEW  30278  pwsiga  30502  measiun  30590  dya2iocuni  30654  bnj518  31263  bnj1137  31370  bnj1136  31372  bnj1413  31410  bnj1417  31416  bnj60  31437  erdszelem8  31487  cvmsss2  31563  cvmfolem  31568  dfon2lem8  32000  dfon2lem9  32001  dfon2  32002  rdgprc  32005  trpredtr  32035  trpredmintr  32036  trpredelss  32037  dftrpred3g  32038  trpredpo  32040  trpredrec  32043  frr3g  32085  frrlem5b  32091  frrlem5d  32093  sltval2  32115  nolesgn2ores  32131  nosupres  32159  nosupbnd2lem1  32167  scutun12  32223  nn0prpwlem  32623  ntruni  32628  clsint2  32630  fneint  32649  fnessref  32658  refssfne  32659  neibastop1  32660  neibastop2lem  32661  bj-0int  33361  bj-ismooredr2  33371  relowlpssretop  33523  heicant  33757  mblfinlem1  33759  ftc2nc  33807  sdclem2  33851  fdc  33854  seqpo  33856  prdsbnd  33905  heibor  33933  rrnequiv  33947  0idl  34137  intidl  34141  unichnidl  34143  prnc  34179  uniqsALTV  34425  lsmcv2  34819  lcvexchlem4  34827  lcvexchlem5  34828  eqlkr  34889  paddclN  35631  pclfinN  35689  ldilcnv  35904  ldilco  35905  cdleme25dN  36146  cdlemj2  36612  tendocan  36614  erng1lem  36777  erngdvlem4-rN  36789  dihord2pre  37016  dihglblem2N  37085  dochvalr  37148  hdmap14lem12  37673  hdmap14lem13  37674  pellfundre  37947  pellfundge  37948  pellfundlb  37950  dford3lem1  38095  aomclem2  38127  pwinfi3  38370  iunrelexp0  38496  iunrelexpmin1  38502  iunrelexpmin2  38506  dftrcl3  38514  cnvtrclfv  38518  trclimalb2  38520  dfrtrcl3  38527  ntrneiel2  38886  ntrneik4w  38900  ntrrn  38922  gneispa  38930  gneispb  38931  addrcom  39181  iunconnlem2  39670  ssuzfz  40063  dvmptfprod  40663  dvnprodlem3  40666  funressnfv  41714  tz6.12-afv  41759  otiunsndisjX  41806  iccpartltu  41871  iccpartgtl  41872  iccpartleu  41874  iccpartgel  41875  fargshiftf  41886  fargshiftfva  41889  sbgoldbst  42176  bgoldbtbnd  42207  tgblthelfgott  42213  tgblthelfgottOLD  42219  nnsgrp  42327  ellcoellss  42734  lindsrng01  42767  suppdm  42810  nn0sumshdiglem1  42925  setrec2fun  42949
  Copyright terms: Public domain W3C validator