Theorem ralrimiv 3151

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ral 3068

This theorem is referenced by:  ralrimiva  3152  ralrimivw  3156  ralrimdv  3158  reximdvaiOLD  3172  ralrimivv  3206  rr19.3v  3680  class2seteq  3726  rabssdv  4098  rzalALT  4533  disjord  5155  disjiund  5157  trin  5295  ralxfrALT  5433  otiunsndisj  5539  onmindif  6487  fnprb  7245  fntpb  7246  f1cdmsn  7318  ssorduni  7814  onminex  7838  onmindif2  7843  sucexeloniOLD  7846  suceloniOLD  7848  limuni3  7889  frxp  8167  poxp  8169  sexp2  8187  sexp3  8194  wfrlem15OLD  8379  onfununi  8397  onnseq  8400  tfrlem12  8445  tz7.48-2  8498  oaass  8617  omass  8636  oelim2  8651  oelimcl  8656  oaabs2  8705  omabs  8707  undifixp  8992  dom2lem  9052  isinf  9323  isinfOLD  9324  unblem4  9359  unbnn2  9361  marypha1lem  9502  supiso  9544  ordiso2  9584  card2inf  9624  elirrv  9665  wemapwe  9766  ttrclss  9789  trcl  9797  frr3g  9825  tz9.13  9860  rankval3b  9895  rankunb  9919  rankuni2b  9922  scott0  9955  updjud  10003  dfac8alem  10098  carduniima  10165  alephsmo  10171  alephval3  10179  iunfictbso  10183  dfac3  10190  dfac5lem5  10196  dfac12r  10216  dfac12k  10217  kmlem4  10223  kmlem11  10230  cfsuc  10326  cofsmo  10338  cfsmolem  10339  coftr  10342  alephsing  10345  infpssrlem3  10374  fin23lem30  10411  isf32lem2  10423  isf32lem3  10424  isf34lem6  10449  fin1a2lem11  10479  fin1a2lem13  10481  fin1a2s  10483  axcc2lem  10505  domtriomlem  10511  axdc3lem2  10520  axdc4lem  10524  axcclem  10526  axdclem2  10589  iundom2g  10609  uniimadom  10613  cardmin  10633  alephval2  10641  alephreg  10651  fpwwe2lem11  10710  wunex2  10807  wuncval2  10816  tskwe2  10842  inar1  10844  tskuni  10852  gruun  10875  intgru  10883  grutsk1  10890  genpcl  11077  ltexprlem5  11109  suplem1pr  11121  supexpr  11123  supsrlem  11180  axpre-sup  11238  negfi  12244  supaddc  12262  supadd  12263  supmul1  12264  supmullem1  12265  supmul  12267  peano5nni  12296  uzind  12735  zindd  12744  uzwo  12976  lbzbi  13001  xrsupsslem  13369  xrinfmsslem  13370  supxrun  13378  supxrpnf  13380  supxrunb1  13381  supxrunb2  13382  icoshftf1o  13534  flval3  13866  axdc4uzlem  14034  tpfo  14549  wrdnfi  14596  ccatrn  14637  ccatalpha  14641  2cshw  14861  cshweqrep  14869  s3iunsndisj  15017  rtrclreclem4  15110  dfrtrcl2  15111  01sqrexlem1  15291  01sqrexlem6  15296  fsum0diag2  15831  alzdvds  16368  gcdcllem1  16545  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  maxprmfct  16756  hashgcdeq  16836  unbenlem  16955  vdwlem6  17033  vdwlem10  17037  firest  17492  mrieqv2d  17697  iscatd  17731  initoeu2  18083  setcmon  18154  setcepi  18155  fullestrcsetc  18220  fullsetcestrc  18235  isglbd  18579  isacs4lem  18614  acsfiindd  18623  acsmapd  18624  psss  18650  sgrpidmnd  18777  pwmnd  18972  ghmrn  19269  ghmpreima  19278  cntz2ss  19375  symgextres  19467  psgnunilem2  19537  lsmsubg  19696  efgsfo  19781  gsumzaddlem  19963  gsummptnn0fzfv  20029  dmdprdd  20043  dprd2da  20086  ablsimpgprmd  20159  imasring  20353  01eq0ring  20556  isabvd  20835  issrngd  20878  islssd  20956  lbsextlem3  21185  lbsextlem4  21186  lidldvgen  21367  pzriprnglem4  21518  pzriprnglem7  21521  pzriprnglem13  21527  psgnghm  21621  isphld  21695  frlmsslsp  21839  mp2pm2mplem4  22836  tgcl  22997  distop  23023  indistopon  23029  pptbas  23036  toponmre  23122  opnnei  23149  neiuni  23151  neindisj2  23152  ordtrest2  23233  cnpnei  23293  cnindis  23321  cmpcld  23431  uncmp  23432  hauscmplem  23435  2ndc1stc  23480  1stcrest  23482  1stcelcls  23490  llyrest  23514  nllyrest  23515  cldllycmp  23524  reftr  23543  locfincf  23560  comppfsc  23561  txcls  23633  ptpjcn  23640  ptclsg  23644  dfac14lem  23646  xkoccn  23648  txlly  23665  txnlly  23666  ptrescn  23668  tx1stc  23679  xkoco1cn  23686  xkoco2cn  23687  xkococn  23689  xkoinjcn  23716  qtopeu  23745  hmeofval  23787  ordthmeolem  23830  isfild  23887  fbasrn  23913  trfil2  23916  flimclslem  24013  fclsrest  24053  fclscf  24054  flimfcls  24055  alexsubALTlem1  24076  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALT  24080  qustgpopn  24149  isxmetd  24357  imasdsf1olem  24404  blcls  24540  prdsxmslem2  24563  metustfbas  24591  dscmet  24606  nrmmetd  24608  reperflem  24859  reconnlem2  24868  xrge0tsms  24875  fsumcn  24913  cnheibor  25006  tcphcph  25290  lmmbr  25311  caubl  25361  ivthlem1  25505  ovolctb  25544  ovoliunlem2  25557  ovolscalem1  25567  ovolicc2  25576  voliunlem3  25606  ismbfd  25693  mbfimaopnlem  25709  itg2le  25794  ellimc2  25932  c1liplem1  26055  plyeq0lem  26269  dgreq0  26325  aannenlem1  26388  pilem2  26514  cxpcn3lem  26808  scvxcvx  27047  musum  27252  fsumdvdsmul  27256  dchrisum0flb  27572  ostth2lem2  27696  sltval2  27719  nolesgn2ores  27735  nogesgn1ores  27737  nosupres  27770  nosupbnd2lem1  27778  noinfres  27785  noinfbnd2lem1  27793  scutun12  27873  madebdayim  27944  precsexlem9  28257  noseqind  28316  zs12bday  28442  numedglnl  29179  upgrreslem  29339  umgrreslem  29340  nbuhgr  29378  nbumgr  29382  uhgrnbgr0nb  29389  nbusgrf1o0  29404  uvtxnbgrvtx  29428  cusgrfilem2  29492  uspgr2wlkeq  29682  wwlks  29868  iswwlksnon  29886  rusgr0edg  30006  clwwlkccatlem  30021  clwwisshclwwslem  30046  clwwlkn  30058  clwwlknon  30122  3cyclfrgrrn  30318  vdgn1frgrv3  30329  2wspmdisj  30369  numclwlk2lem2f1o  30411  frgrregord013  30427  htthlem  30949  ocsh  31315  shintcli  31361  pjss2coi  32196  pjnormssi  32200  pjclem4  32231  pj3si  32239  pj3cor1i  32241  strlem3a  32284  strb  32290  hstrlem3a  32292  hstrbi  32298  spansncv2  32325  mdsl1i  32353  cvmdi  32356  mdexchi  32367  h1da  32381  mdsymlem6  32440  sumdmdii  32447  dmdbr5ati  32454  isoun  32713  supssd  32723  infssd  32724  xrge0tsmsd  33041  ordtrest2NEW  33869  pwsiga  34094  measiun  34182  dya2iocuni  34248  bnj518  34862  bnj1137  34971  bnj1136  34973  bnj1413  35011  bnj1417  35017  bnj60  35038  gblacfnacd  35075  subgrwlk  35100  erdszelem8  35166  cvmsss2  35242  cvmfolem  35247  fmlasucdisj  35367  satfun  35379  dfon2lem8  35754  dfon2lem9  35755  dfon2  35756  rdgprc  35758  nn0prpwlem  36288  ntruni  36293  clsint2  36295  fneint  36314  fnessref  36323  refssfne  36324  neibastop1  36325  neibastop2lem  36326  bj-0int  37067  bj-ismooredr  37075  relowlpssretop  37330  fvineqsneu  37377  fvineqsneq  37378  heicant  37615  mblfinlem1  37617  ftc2nc  37662  sdclem2  37702  fdc  37705  seqpo  37707  prdsbnd  37753  heibor  37781  rrnequiv  37795  0idl  37985  intidl  37989  unichnidl  37991  prnc  38027  uniqsALTV  38285  refressn  38399  lsmcv2  38985  lcvexchlem4  38993  lcvexchlem5  38994  eqlkr  39055  paddclN  39799  pclfinN  39857  ldilcnv  40072  ldilco  40073  cdleme25dN  40313  cdlemj2  40779  tendocan  40781  erng1lem  40944  erngdvlem4-rN  40956  dihord2pre  41182  dihglblem2N  41251  dochvalr  41314  hdmap14lem12  41836  hdmap14lem13  41837  supinf  42237  fsuppind  42545  pellfundre  42837  pellfundge  42838  pellfundlb  42840  dford3lem1  42983  aomclem2  43012  oaabsb  43256  cantnf2  43287  ofoafg  43316  naddcnff  43324  naddwordnexlem3  43361  naddwordnexlem4  43363  pwinfi3  43525  iunrelexp0  43664  iunrelexpmin1  43670  iunrelexpmin2  43674  dftrcl3  43682  cnvtrclfv  43686  trclimalb2  43688  dfrtrcl3  43695  ntrneiel2  44048  ntrneik4w  44062  ntrrn  44084  gneispa  44092  gneispb  44093  addrcom  44444  iunconnlem2  44906  ssuzfz  45264  dvmptfprod  45866  dvnprodlem3  45869  funressnfv  46958  cfsetsnfsetfo  46975  tz6.12-afv  47088  tz6.12-afv2  47155  otiunsndisjX  47194  uniimaprimaeqfv  47256  iccpartltu  47299  iccpartgtl  47300  iccpartleu  47302  iccpartgel  47303  fargshiftf  47314  fargshiftfva  47317  sbgoldbst  47652  bgoldbtbnd  47683  tgblthelfgott  47689  isuspgrim0  47756  isuspgrimlem  47758  grimuhgr  47762  grimco  47764  gricushgr  47770  grtriclwlk3  47796  uspgrlim  47816  grlicsym  47830  nnsgrp  47900  ellcoellss  48164  lindsrng01  48197  suppdm  48239  nn0sumshdiglem1  48355  setrec2fun  48784