Theorem ralrimiv 3124

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

Step	Hyp	Ref	Expression
1		ax-5 1870	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	hbralrimi 3123	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2051  ∀wral 3081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870

This theorem depends on definitions:  df-bi 199  df-ral 3086

This theorem is referenced by:  ralrimiva  3125  ralrimivw  3126  r19.27vOLD  3128  ralrimdv  3131  ralrimivv  3133  reximdvai  3210  raleleq  3360  rr19.3v  3568  rabssdv  3934  rzal  4330  disjord  4914  disjiund  4916  trin  5036  class2seteq  5105  ralxfrALT  5165  otiunsndisj  5262  onmindif  6115  fnprb  6795  fntpb  6796  ssorduni  7314  onminex  7336  onmindif2  7341  suceloni  7342  limuni3  7381  frxp  7623  poxp  7625  wfrlem15  7771  onfununi  7780  onnseq  7783  tfrlem12  7827  tz7.48-2  7879  oaass  7986  omass  8005  oelim2  8020  oelimcl  8025  oaabs2  8070  omabs  8072  undifixp  8293  dom2lem  8344  isinf  8524  unblem4  8566  unbnn2  8568  marypha1lem  8690  supiso  8732  ordiso2  8772  card2inf  8812  elirrv  8853  wemapwe  8952  trcl  8962  tz9.13  9012  rankval3b  9047  rankunb  9071  rankuni2b  9074  scott0  9107  updjud  9155  dfac8alem  9247  carduniima  9314  alephsmo  9320  alephval3  9328  iunfictbso  9332  dfac3  9339  dfac5lem5  9345  dfac12r  9364  dfac12k  9365  kmlem4  9371  kmlem11  9378  cfsuc  9475  cofsmo  9487  cfsmolem  9488  coftr  9491  alephsing  9494  infpssrlem3  9523  fin23lem30  9560  isf32lem2  9572  isf32lem3  9573  isf34lem6  9598  fin1a2lem11  9628  fin1a2lem13  9630  fin1a2s  9632  axcc2lem  9654  domtriomlem  9660  axdc3lem2  9669  axdc4lem  9673  axcclem  9675  axdclem2  9738  iundom2g  9758  uniimadom  9762  cardmin  9782  alephval2  9790  alephreg  9800  fpwwe2lem12  9859  wunex2  9956  wuncval2  9965  tskwe2  9991  inar1  9993  tskuni  10001  gruun  10024  intgru  10032  grutsk1  10039  genpcl  10226  ltexprlem5  10258  suplem1pr  10270  supexpr  10272  supsrlem  10329  axpre-sup  10387  negfi  11388  fiminreOLD  11389  supaddc  11407  supadd  11408  supmul1  11409  supmullem1  11410  supmul  11412  peano5nni  11440  uzind  11885  zindd  11894  uzwo  12123  lbzbi  12148  xrsupsslem  12514  xrinfmsslem  12515  supxrun  12523  supxrpnf  12525  supxrunb1  12526  supxrunb2  12527  icoshftf1o  12674  flval3  12998  axdc4uzlem  13164  wrdnfi  13708  ccatrn  13750  ccatalpha  13754  2cshw  14035  cshweqrep  14043  s3iunsndisj  14187  rtrclreclem4  14279  dfrtrcl2  14280  sqrlem1  14461  sqrlem6  14466  fsum0diag2  14996  alzdvds  15528  gcdcllem1  15706  lcmfunsnlem2lem1  15836  lcmfunsnlem2lem2  15837  maxprmfct  15907  hashgcdeq  15980  unbenlem  16098  vdwlem6  16176  vdwlem10  16180  firest  16560  mrieqv2d  16780  iscatd  16814  initoeu2  17146  setcmon  17217  setcepi  17218  fullestrcsetc  17271  fullsetcestrc  17286  isglbd  17597  isacs4lem  17648  acsfiindd  17657  acsmapd  17658  psss  17694  ghmrn  18154  ghmpreima  18163  cntz2ss  18246  symgextres  18326  psgnunilem2  18397  lsmsubg  18552  efgsfo  18636  gsumzaddlem  18806  gsummptnn0fzfv  18869  dmdprdd  18883  dprd2da  18926  imasring  19104  isabvd  19325  issrngd  19366  islssd  19441  lbsextlem3  19666  lbsextlem4  19667  lidldvgen  19761  psgnghm  20441  isphld  20515  frlmsslsp  20657  mp2pm2mplem4  21136  tgcl  21296  distop  21322  indistopon  21328  pptbas  21335  toponmre  21420  opnnei  21447  neiuni  21449  neindisj2  21450  ordtrest2  21531  cnpnei  21591  cnindis  21619  cmpcld  21729  uncmp  21730  hauscmplem  21733  2ndc1stc  21778  1stcrest  21780  1stcelcls  21788  llyrest  21812  nllyrest  21813  cldllycmp  21822  reftr  21841  locfincf  21858  comppfsc  21859  txcls  21931  ptpjcn  21938  ptclsg  21942  dfac14lem  21944  xkoccn  21946  txlly  21963  txnlly  21964  ptrescn  21966  tx1stc  21977  xkoco1cn  21984  xkoco2cn  21985  xkococn  21987  xkoinjcn  22014  qtopeu  22043  hmeofval  22085  ordthmeolem  22128  isfild  22185  fbasrn  22211  trfil2  22214  flimclslem  22311  fclsrest  22351  fclscf  22352  flimfcls  22353  alexsubALTlem1  22374  alexsubALTlem2  22375  alexsubALTlem3  22376  alexsubALT  22378  qustgpopn  22446  isxmetd  22654  imasdsf1olem  22701  blcls  22834  prdsxmslem2  22857  metustfbas  22885  dscmet  22900  nrmmetd  22902  reperflem  23144  reconnlem2  23153  xrge0tsms  23160  fsumcn  23196  cnheibor  23277  tcphcph  23558  lmmbr  23579  caubl  23629  ivthlem1  23770  ovolctb  23809  ovoliunlem2  23822  ovolscalem1  23832  ovolicc2  23841  voliunlem3  23871  ismbfd  23958  mbfimaopnlem  23974  itg2le  24058  ellimc2  24193  c1liplem1  24311  plyeq0lem  24518  dgreq0  24573  aannenlem1  24635  pilem2  24758  cxpcn3lem  25044  scvxcvx  25280  musum  25485  dchrisum0flb  25803  ostth2lem2  25927  numedglnl  26647  upgrreslem  26804  umgrreslem  26805  nbuhgr  26843  nbumgr  26847  uhgrnbgr0nb  26854  nbusgrf1o0  26869  uvtxnbgrvtx  26893  cusgrfilem2  26956  uspgr2wlkeq  27145  wwlks  27336  iswwlksnon  27354  rusgr0edg  27494  clwwlkccatlem  27510  clwwisshclwwslem  27544  clwwlkn  27556  clwwlknon  27633  3cyclfrgrrn  27835  vdgn1frgrv3  27846  2wspmdisj  27886  numclwlk2lem2f1o  27947  numclwlk2lem2f1oOLD  27950  frgrregord013  27967  htthlem  28488  ocsh  28856  shintcli  28902  pjss2coi  29737  pjnormssi  29741  pjclem4  29772  pj3si  29780  pj3cor1i  29782  strlem3a  29825  strb  29831  hstrlem3a  29833  hstrbi  29839  spansncv2  29866  mdsl1i  29894  cvmdi  29897  mdexchi  29908  h1da  29922  mdsymlem6  29981  sumdmdii  29988  dmdbr5ati  29995  isoun  30213  supssd  30221  infssd  30222  xrge0tsmsd  30562  ordtrest2NEW  30842  pwsiga  31066  measiun  31154  dya2iocuni  31218  bnj518  31837  bnj1137  31944  bnj1136  31946  bnj1413  31984  bnj1417  31990  bnj60  32011  erdszelem8  32067  cvmsss2  32143  cvmfolem  32148  dfon2lem8  32592  dfon2lem9  32593  dfon2  32594  rdgprc  32597  trpredtr  32627  trpredmintr  32628  trpredelss  32629  dftrpred3g  32630  trpredpo  32632  trpredrec  32635  frr3g  32679  sltval2  32721  nolesgn2ores  32737  nosupres  32765  nosupbnd2lem1  32773  scutun12  32829  nn0prpwlem  33228  ntruni  33233  clsint2  33235  fneint  33254  fnessref  33263  refssfne  33264  neibastop1  33265  neibastop2lem  33266  bj-0int  33940  bj-ismooredr  33949  bj-ismooredr2  33950  relowlpssretop  34124  fvineqsneu  34170  fvineqsneq  34171  heicant  34405  mblfinlem1  34407  ftc2nc  34454  sdclem2  34496  fdc  34499  seqpo  34501  prdsbnd  34550  heibor  34578  rrnequiv  34592  0idl  34782  intidl  34786  unichnidl  34788  prnc  34824  uniqsALTV  35068  lsmcv2  35647  lcvexchlem4  35655  lcvexchlem5  35656  eqlkr  35717  paddclN  36460  pclfinN  36518  ldilcnv  36733  ldilco  36734  cdleme25dN  36974  cdlemj2  37440  tendocan  37442  erng1lem  37605  erngdvlem4-rN  37617  dihord2pre  37843  dihglblem2N  37912  dochvalr  37975  hdmap14lem12  38497  hdmap14lem13  38498  pellfundre  38912  pellfundge  38913  pellfundlb  38915  dford3lem1  39057  aomclem2  39089  pwinfi3  39322  iunrelexp0  39448  iunrelexpmin1  39454  iunrelexpmin2  39458  dftrcl3  39466  cnvtrclfv  39470  trclimalb2  39472  dfrtrcl3  39479  ntrneiel2  39837  ntrneik4w  39851  ntrrn  39873  gneispa  39881  gneispb  39882  ablsimpgprmd  40088  addrcom  40263  iunconnlem2  40725  ssuzfz  41078  dvmptfprod  41692  dvnprodlem3  41695  funressnfv  42715  tz6.12-afv  42810  tz6.12-afv2  42877  otiunsndisjX  42916  iccpartltu  42989  iccpartgtl  42990  iccpartleu  42992  iccpartgel  42993  fargshiftf  43004  fargshiftfva  43007  sbgoldbst  43343  bgoldbtbnd  43374  tgblthelfgott  43380  isomushgr  43391  nnsgrp  43484  ellcoellss  43889  lindsrng01  43922  suppdm  43965  nn0sumshdiglem1  44081  setrec2fun  44194