Theorem ralrimiv 3135

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 1906	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		ralrimiv.1	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	hbralrimi 3134	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2099  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-ral 3052

This theorem is referenced by:  ralrimiva  3136  ralrimivw  3140  ralrimdv  3142  reximdvaiOLD  3156  ralrimivv  3189  rr19.3v  3654  class2seteq  3698  rabssdv  4071  rzalALT  4514  disjord  5141  disjiund  5143  trin  5282  ralxfrALT  5419  otiunsndisj  5526  onmindif  6468  fnprb  7225  fntpb  7226  f1cdmsn  7296  ssorduni  7787  onminex  7811  onmindif2  7816  sucexeloniOLD  7819  suceloniOLD  7821  limuni3  7862  frxp  8140  poxp  8142  sexp2  8160  sexp3  8167  wfrlem15OLD  8353  onfununi  8371  onnseq  8374  tfrlem12  8419  tz7.48-2  8472  oaass  8591  omass  8610  oelim2  8625  oelimcl  8630  oaabs2  8679  omabs  8681  undifixp  8963  dom2lem  9023  isinf  9294  isinfOLD  9295  unblem4  9332  unbnn2  9334  marypha1lem  9476  supiso  9518  ordiso2  9558  card2inf  9598  elirrv  9639  wemapwe  9740  ttrclss  9763  trcl  9771  frr3g  9799  tz9.13  9834  rankval3b  9869  rankunb  9893  rankuni2b  9896  scott0  9929  updjud  9977  dfac8alem  10072  carduniima  10139  alephsmo  10145  alephval3  10153  iunfictbso  10157  dfac3  10164  dfac5lem5  10170  dfac12r  10189  dfac12k  10190  kmlem4  10196  kmlem11  10203  cfsuc  10300  cofsmo  10312  cfsmolem  10313  coftr  10316  alephsing  10319  infpssrlem3  10348  fin23lem30  10385  isf32lem2  10397  isf32lem3  10398  isf34lem6  10423  fin1a2lem11  10453  fin1a2lem13  10455  fin1a2s  10457  axcc2lem  10479  domtriomlem  10485  axdc3lem2  10494  axdc4lem  10498  axcclem  10500  axdclem2  10563  iundom2g  10583  uniimadom  10587  cardmin  10607  alephval2  10615  alephreg  10625  fpwwe2lem11  10684  wunex2  10781  wuncval2  10790  tskwe2  10816  inar1  10818  tskuni  10826  gruun  10849  intgru  10857  grutsk1  10864  genpcl  11051  ltexprlem5  11083  suplem1pr  11095  supexpr  11097  supsrlem  11154  axpre-sup  11212  negfi  12215  supaddc  12233  supadd  12234  supmul1  12235  supmullem1  12236  supmul  12238  peano5nni  12267  uzind  12706  zindd  12715  uzwo  12947  lbzbi  12972  xrsupsslem  13340  xrinfmsslem  13341  supxrun  13349  supxrpnf  13351  supxrunb1  13352  supxrunb2  13353  icoshftf1o  13505  flval3  13835  axdc4uzlem  14003  wrdnfi  14556  ccatrn  14597  ccatalpha  14601  2cshw  14821  cshweqrep  14829  s3iunsndisj  14973  rtrclreclem4  15066  dfrtrcl2  15067  01sqrexlem1  15247  01sqrexlem6  15252  fsum0diag2  15787  alzdvds  16322  gcdcllem1  16499  lcmfunsnlem2lem1  16639  lcmfunsnlem2lem2  16640  maxprmfct  16710  hashgcdeq  16791  unbenlem  16910  vdwlem6  16988  vdwlem10  16992  firest  17447  mrieqv2d  17652  iscatd  17686  initoeu2  18038  setcmon  18109  setcepi  18110  fullestrcsetc  18175  fullsetcestrc  18190  isglbd  18534  isacs4lem  18569  acsfiindd  18578  acsmapd  18579  psss  18605  sgrpidmnd  18732  pwmnd  18927  ghmrn  19223  ghmpreima  19232  cntz2ss  19329  symgextres  19423  psgnunilem2  19493  lsmsubg  19652  efgsfo  19737  gsumzaddlem  19919  gsummptnn0fzfv  19985  dmdprdd  19999  dprd2da  20042  ablsimpgprmd  20115  imasring  20309  01eq0ring  20512  isabvd  20791  issrngd  20834  islssd  20912  lbsextlem3  21141  lbsextlem4  21142  lidldvgen  21323  pzriprnglem4  21474  pzriprnglem7  21477  pzriprnglem13  21483  psgnghm  21576  isphld  21650  frlmsslsp  21794  mp2pm2mplem4  22802  tgcl  22963  distop  22989  indistopon  22995  pptbas  23002  toponmre  23088  opnnei  23115  neiuni  23117  neindisj2  23118  ordtrest2  23199  cnpnei  23259  cnindis  23287  cmpcld  23397  uncmp  23398  hauscmplem  23401  2ndc1stc  23446  1stcrest  23448  1stcelcls  23456  llyrest  23480  nllyrest  23481  cldllycmp  23490  reftr  23509  locfincf  23526  comppfsc  23527  txcls  23599  ptpjcn  23606  ptclsg  23610  dfac14lem  23612  xkoccn  23614  txlly  23631  txnlly  23632  ptrescn  23634  tx1stc  23645  xkoco1cn  23652  xkoco2cn  23653  xkococn  23655  xkoinjcn  23682  qtopeu  23711  hmeofval  23753  ordthmeolem  23796  isfild  23853  fbasrn  23879  trfil2  23882  flimclslem  23979  fclsrest  24019  fclscf  24020  flimfcls  24021  alexsubALTlem1  24042  alexsubALTlem2  24043  alexsubALTlem3  24044  alexsubALT  24046  qustgpopn  24115  isxmetd  24323  imasdsf1olem  24370  blcls  24506  prdsxmslem2  24529  metustfbas  24557  dscmet  24572  nrmmetd  24574  reperflem  24825  reconnlem2  24834  xrge0tsms  24841  fsumcn  24879  cnheibor  24972  tcphcph  25256  lmmbr  25277  caubl  25327  ivthlem1  25471  ovolctb  25510  ovoliunlem2  25523  ovolscalem1  25533  ovolicc2  25542  voliunlem3  25572  ismbfd  25659  mbfimaopnlem  25675  itg2le  25760  ellimc2  25897  c1liplem1  26020  plyeq0lem  26237  dgreq0  26293  aannenlem1  26356  pilem2  26482  cxpcn3lem  26775  scvxcvx  27014  musum  27219  fsumdvdsmul  27223  dchrisum0flb  27539  ostth2lem2  27663  sltval2  27686  nolesgn2ores  27702  nogesgn1ores  27704  nosupres  27737  nosupbnd2lem1  27745  noinfres  27752  noinfbnd2lem1  27760  scutun12  27840  madebdayim  27911  precsexlem9  28214  noseqind  28266  numedglnl  29080  upgrreslem  29240  umgrreslem  29241  nbuhgr  29279  nbumgr  29283  uhgrnbgr0nb  29290  nbusgrf1o0  29305  uvtxnbgrvtx  29329  cusgrfilem2  29393  uspgr2wlkeq  29583  wwlks  29769  iswwlksnon  29787  rusgr0edg  29907  clwwlkccatlem  29922  clwwisshclwwslem  29947  clwwlkn  29959  clwwlknon  30023  3cyclfrgrrn  30219  vdgn1frgrv3  30230  2wspmdisj  30270  numclwlk2lem2f1o  30312  frgrregord013  30328  htthlem  30850  ocsh  31216  shintcli  31262  pjss2coi  32097  pjnormssi  32101  pjclem4  32132  pj3si  32140  pj3cor1i  32142  strlem3a  32185  strb  32191  hstrlem3a  32193  hstrbi  32199  spansncv2  32226  mdsl1i  32254  cvmdi  32257  mdexchi  32268  h1da  32282  mdsymlem6  32341  sumdmdii  32348  dmdbr5ati  32355  isoun  32613  supssd  32623  infssd  32624  xrge0tsmsd  32926  ordtrest2NEW  33738  pwsiga  33963  measiun  34051  dya2iocuni  34117  bnj518  34731  bnj1137  34840  bnj1136  34842  bnj1413  34880  bnj1417  34886  bnj60  34907  gblacfnacd  34935  subgrwlk  34960  erdszelem8  35026  cvmsss2  35102  cvmfolem  35107  fmlasucdisj  35227  satfun  35239  dfon2lem8  35614  dfon2lem9  35615  dfon2  35616  rdgprc  35618  nn0prpwlem  36034  ntruni  36039  clsint2  36041  fneint  36060  fnessref  36069  refssfne  36070  neibastop1  36071  neibastop2lem  36072  bj-0int  36808  bj-ismooredr  36816  relowlpssretop  37071  fvineqsneu  37118  fvineqsneq  37119  heicant  37356  mblfinlem1  37358  ftc2nc  37403  sdclem2  37443  fdc  37446  seqpo  37448  prdsbnd  37494  heibor  37522  rrnequiv  37536  0idl  37726  intidl  37730  unichnidl  37732  prnc  37768  uniqsALTV  38027  refressn  38141  lsmcv2  38727  lcvexchlem4  38735  lcvexchlem5  38736  eqlkr  38797  paddclN  39541  pclfinN  39599  ldilcnv  39814  ldilco  39815  cdleme25dN  40055  cdlemj2  40521  tendocan  40523  erng1lem  40686  erngdvlem4-rN  40698  dihord2pre  40924  dihglblem2N  40993  dochvalr  41056  hdmap14lem12  41578  hdmap14lem13  41579  supinf  41966  fsuppind  42062  pellfundre  42538  pellfundge  42539  pellfundlb  42541  dford3lem1  42684  aomclem2  42716  oaabsb  42960  cantnf2  42991  ofoafg  43020  naddcnff  43028  naddwordnexlem3  43066  naddwordnexlem4  43068  pwinfi3  43230  iunrelexp0  43369  iunrelexpmin1  43375  iunrelexpmin2  43379  dftrcl3  43387  cnvtrclfv  43391  trclimalb2  43393  dfrtrcl3  43400  ntrneiel2  43753  ntrneik4w  43767  ntrrn  43789  gneispa  43797  gneispb  43798  addrcom  44149  iunconnlem2  44611  ssuzfz  44964  dvmptfprod  45566  dvnprodlem3  45569  funressnfv  46658  cfsetsnfsetfo  46675  tz6.12-afv  46786  tz6.12-afv2  46853  otiunsndisjX  46892  uniimaprimaeqfv  46954  iccpartltu  46997  iccpartgtl  46998  iccpartleu  47000  iccpartgel  47001  fargshiftf  47012  fargshiftfva  47015  sbgoldbst  47350  bgoldbtbnd  47381  tgblthelfgott  47387  isuspgrim0  47451  isuspgrimlem  47453  grimuhgr  47457  grimco  47459  gricushgr  47465  grlicsym  47503  nnsgrp  47554  ellcoellss  47818  lindsrng01  47851  suppdm  47893  nn0sumshdiglem1  48009  setrec2fun  48438