Theorem ralrimiv 3132

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

Syntax hints:   → wi 4   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 209  df-ral 3056

This theorem is referenced by:  ralrimiva  3133  ralrimivw  3137  ralrimdv  3139  ralrimivv  3182  rr19.3v  3607  class2seteq  3647  rabssdv  4008  rzalALT  4426  r19.3rzv  4434  disjord  5064  disjiund  5066  trun  5193  trin  5194  ralxfrALT  5347  otiunsndisj  5464  onmindif  6408  fnprb  7156  fntpb  7157  f1cdmsn  7230  ssorduni  7726  onminex  7749  onmindif2  7754  limuni3  7796  frxp  8070  poxp  8072  sexp2  8090  sexp3  8097  onfununi  8275  onnseq  8278  tfrlem12  8322  tz7.48-2  8375  oaass  8490  omass  8509  oelim2  8525  oelimcl  8530  oaabs2  8579  omabs  8581  uniqs  8714  undifixp  8876  dom2lem  8933  isinf  9169  unblem4  9199  unbnn2  9201  marypha1lem  9340  supssd  9370  supiso  9383  infssd  9401  ordiso2  9424  card2inf  9464  elirrvOLDOLD  9508  wemapwe  9613  ttrclss  9636  trcl  9644  frr3g  9675  tz9.13  9710  rankval3b  9745  rankunb  9769  rankuni2b  9772  scott0  9805  updjud  9853  dfac8alem  9946  carduniima  10013  alephsmo  10019  alephval3  10027  iunfictbso  10031  dfac3  10038  dfac5lem5  10044  dfac12r  10064  dfac12k  10065  kmlem4  10071  kmlem11  10078  cfsuc  10174  cofsmo  10186  cfsmolem  10187  coftr  10190  alephsing  10193  infpssrlem3  10222  fin23lem30  10259  isf32lem2  10271  isf32lem3  10272  isf34lem6  10297  fin1a2lem11  10327  fin1a2lem13  10329  fin1a2s  10331  axcc2lem  10353  domtriomlem  10359  axdc3lem2  10368  axdc4lem  10372  axcclem  10374  axdclem2  10437  iundom2g  10457  uniimadom  10461  cardmin  10481  alephval2  10490  alephreg  10500  fpwwe2lem11  10559  wunex2  10656  wuncval2  10665  tskwe2  10691  inar1  10693  tskuni  10701  gruun  10724  intgru  10732  grutsk1  10739  genpcl  10926  ltexprlem5  10958  suplem1pr  10970  supexpr  10972  supsrlem  11029  axpre-sup  11087  negfi  12100  supaddc  12118  supadd  12119  supmul1  12120  supmullem1  12121  supmul  12123  peano5nni  12172  uzind  12616  zindd  12625  uzwo  12856  lbzbi  12881  xrsupsslem  13254  xrinfmsslem  13255  supxrun  13263  supxrpnf  13265  supxrunb1  13266  supxrunb2  13267  icoshftf1o  13422  flval3  13769  axdc4uzlem  13940  tpfo  14457  wrdnfi  14505  ccatrn  14547  ccatalpha  14551  2cshw  14770  cshweqrep  14778  s3iunsndisj  14925  rtrclreclem4  15018  dfrtrcl2  15019  01sqrexlem1  15199  01sqrexlem6  15204  fsum0diag2  15740  alzdvds  16284  gcdcllem1  16463  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  maxprmfct  16674  hashgcdeq  16755  unbenlem  16874  vdwlem6  16952  vdwlem10  16956  firest  17390  mrieqv2d  17600  iscatd  17634  initoeu2  17978  setcmon  18049  setcepi  18050  fullestrcsetc  18112  fullsetcestrc  18127  isglbd  18470  isacs4lem  18505  acsfiindd  18514  acsmapd  18515  psss  18541  sgrpidmnd  18702  pwmnd  18903  ghmrn  19199  ghmpreima  19208  cntz2ss  19305  symgextres  19395  psgnunilem2  19465  lsmsubg  19624  efgsfo  19709  gsumzaddlem  19891  gsummptnn0fzfv  19957  dmdprdd  19971  dprd2da  20014  ablsimpgprmd  20087  imasring  20305  01eq0ring  20506  isabvd  20788  issrngd  20831  islssd  20929  lbsextlem3  21157  lbsextlem4  21158  lidldvgen  21331  pzriprnglem4  21463  pzriprnglem7  21466  pzriprnglem13  21472  psgnghm  21559  isphld  21633  frlmsslsp  21775  mp2pm2mplem4  22796  tgcl  22956  distop  22982  indistopon  22988  pptbas  22995  toponmre  23080  opnnei  23107  neiuni  23109  neindisj2  23110  ordtrest2  23191  cnpnei  23251  cnindis  23279  cmpcld  23389  uncmp  23390  hauscmplem  23393  2ndc1stc  23438  1stcrest  23440  1stcelcls  23448  llyrest  23472  nllyrest  23473  cldllycmp  23482  reftr  23501  locfincf  23518  comppfsc  23519  txcls  23591  ptpjcn  23598  ptclsg  23602  dfac14lem  23604  xkoccn  23606  txlly  23623  txnlly  23624  ptrescn  23626  tx1stc  23637  xkoco1cn  23644  xkoco2cn  23645  xkococn  23647  xkoinjcn  23674  qtopeu  23703  hmeofval  23745  ordthmeolem  23788  isfild  23845  fbasrn  23871  trfil2  23874  flimclslem  23971  fclsrest  24011  fclscf  24012  flimfcls  24013  alexsubALTlem1  24034  alexsubALTlem2  24035  alexsubALTlem3  24036  alexsubALT  24038  qustgpopn  24107  isxmetd  24313  imasdsf1olem  24360  blcls  24493  prdsxmslem2  24516  metustfbas  24544  dscmet  24559  nrmmetd  24561  reperflem  24806  reconnlem2  24815  xrge0tsms  24822  fsumcn  24859  cnheibor  24944  tcphcph  25226  lmmbr  25247  caubl  25297  ivthlem1  25440  ovolctb  25479  ovoliunlem2  25492  ovolscalem1  25502  ovolicc2  25511  voliunlem3  25541  ismbfd  25628  mbfimaopnlem  25644  itg2le  25728  ellimc2  25866  c1liplem1  25985  plyeq0lem  26197  dgreq0  26252  aannenlem1  26316  pilem2  26439  cxpcn3lem  26733  scvxcvx  26971  musum  27176  fsumdvdsmul  27180  dchrisum0flb  27495  ostth2lem2  27619  ltsval2  27642  nolesgn2ores  27658  nogesgn1ores  27660  nosupres  27693  nosupbnd2lem1  27701  noinfres  27708  noinfbnd2lem1  27716  cutsun12  27804  madebdayim  27902  precsexlem9  28229  addonbday  28293  noseqind  28306  z12zsodd  28496  numedglnl  29235  upgrreslem  29395  umgrreslem  29396  nbuhgr  29434  nbumgr  29438  uhgrnbgr0nb  29445  nbusgrf1o0  29460  uvtxnbgrvtx  29484  cusgrfilem2  29547  uspgr2wlkeq  29736  wwlks  29925  iswwlksnon  29943  rusgr0edg  30066  clwwlkccatlem  30081  clwwisshclwwslem  30106  clwwlkn  30118  clwwlknon  30182  3cyclfrgrrn  30378  vdgn1frgrv3  30389  2wspmdisj  30429  numclwlk2lem2f1o  30471  frgrregord013  30487  htthlem  31010  ocsh  31376  shintcli  31422  pjss2coi  32257  pjnormssi  32261  pjclem4  32292  pj3si  32300  pj3cor1i  32302  strlem3a  32345  strb  32351  hstrlem3a  32353  hstrbi  32359  spansncv2  32386  mdsl1i  32414  cvmdi  32417  mdexchi  32428  h1da  32442  mdsymlem6  32501  sumdmdii  32508  dmdbr5ati  32515  isoun  32798  xrge0tsmsd  33158  ordtrest2NEW  34119  pwsiga  34326  measiun  34414  dya2iocuni  34479  bnj518  35083  bnj1137  35192  bnj1136  35194  bnj1413  35232  bnj1417  35238  bnj60  35259  rankval4b  35296  r1filim  35300  trssfir1om  35307  fineqvnttrclselem3  35319  fineqvinfep  35321  tz9.1regs  35330  trssfir1omregs  35332  gblacfnacd  35345  onvf1odlem1  35346  onvf1odlem4  35349  subgrwlk  35375  erdszelem8  35441  cvmsss2  35517  cvmfolem  35522  fmlasucdisj  35642  satfun  35654  dfon2lem8  36031  dfon2lem9  36032  dfon2  36033  rdgprc  36035  nn0prpwlem  36565  ntruni  36570  clsint2  36572  fneint  36591  fnessref  36600  refssfne  36601  neibastop1  36602  neibastop2lem  36603  mh-inf3f1  36784  bj-0int  37474  bj-ismooredr  37482  relowlpssretop  37741  fvineqsneu  37788  fvineqsneq  37789  heicant  38037  mblfinlem1  38039  ftc2nc  38084  sdclem2  38124  fdc  38127  seqpo  38129  prdsbnd  38175  heibor  38203  rrnequiv  38217  0idl  38407  intidl  38411  unichnidl  38413  prnc  38449  refressn  38915  lsmcv2  39536  lcvexchlem4  39544  lcvexchlem5  39545  eqlkr  39606  paddclN  40349  pclfinN  40407  ldilcnv  40622  ldilco  40623  cdleme25dN  40863  cdlemj2  41329  tendocan  41331  erng1lem  41494  erngdvlem4-rN  41506  dihord2pre  41732  dihglblem2N  41801  dochvalr  41864  hdmap14lem12  42386  hdmap14lem13  42387  supinf  42741  fsuppind  43055  pellfundre  43341  pellfundge  43342  pellfundlb  43344  dford3lem1  43486  aomclem2  43515  oaabsb  43754  cantnf2  43785  ofoafg  43814  naddcnff  43822  naddwordnexlem3  43859  naddwordnexlem4  43861  pwinfi3  44022  iunrelexp0  44161  iunrelexpmin1  44167  iunrelexpmin2  44171  dftrcl3  44179  cnvtrclfv  44183  trclimalb2  44185  dfrtrcl3  44192  ntrneiel2  44545  ntrneik4w  44559  ntrrn  44581  gneispa  44589  gneispb  44590  addrcom  44933  iunconnlem2  45393  ssuzfz  45808  dvnprodlem3  46405  funressnfv  47520  cfsetsnfsetfo  47537  tz6.12-afv  47650  tz6.12-afv2  47717  otiunsndisjX  47756  uniimaprimaeqfv  47871  iccpartltu  47914  iccpartgtl  47915  iccpartleu  47917  iccpartgel  47918  fargshiftf  47929  fargshiftfva  47932  sbgoldbst  48283  bgoldbtbnd  48314  tgblthelfgott  48320  grimuhgr  48392  grimco  48394  isuspgrim0  48399  isuspgrimlem  48400  upgrimpths  48414  gricushgr  48422  grtriclwlk3  48450  stgr0  48465  uspgrlim  48497  grlicsym  48518  nnsgrp  48682  ellcoellss  48940  lindsrng01  48973  suppdm  49015  nn0sumshdiglem1  49126  setrec2fun  50196