Theorem ralrimiv 3155

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  ralrimiva  3156  ralrimivw  3160  ralrimdv  3162  ralrimivv  3205  rr19.3v  3624  class2seteq  3665  rabssdv  4025  rzalALT  4454  r19.3rzv  4462  disjord  5096  disjiund  5098  trun  5227  trin  5228  ralxfrALT  5384  otiunsndisj  5501  onmindif  6456  fnprb  7210  fntpb  7211  f1cdmsn  7286  ssorduni  7781  onminex  7804  onmindif2  7809  limuni3  7851  frxp  8127  poxp  8129  sexp2  8147  sexp3  8154  onfununi  8333  onnseq  8336  tfrlem12  8381  tz7.48-2  8434  oaass  8551  omass  8570  oelim2  8586  oelimcl  8591  oaabs2  8640  omabs  8642  uniqs  8776  undifixp  8944  dom2lem  9001  isinf  9238  unblem4  9268  unbnn2  9270  marypha1lem  9406  supssd  9436  supiso  9449  infssd  9467  ordiso2  9490  card2inf  9530  elirrvOLDOLD  9574  wemapwe  9679  ttrclss  9702  trcl  9710  frr3g  9741  tz9.13  9776  rankval3b  9811  rankunb  9835  rankuni2b  9838  scott0b  9879  scott0OLD  9880  updjud  9942  dfac8alem  10035  carduniima  10102  alephsmo  10108  alephval3  10116  iunfictbso  10120  dfac3  10127  dfac5lem5  10133  dfac12r  10152  dfac12k  10153  kmlem4  10159  kmlem11  10166  cfsuc  10262  cofsmo  10274  cfsmolem  10275  coftr  10278  alephsing  10281  infpssrlem3  10310  fin23lem30  10347  isf32lem2  10359  isf32lem3  10360  isf34lem6  10385  fin1a2lem11  10415  fin1a2lem13  10417  fin1a2s  10419  axcc2lem  10441  domtriomlem  10447  axdc3lem2  10456  axdc4lem  10460  axcclem  10462  axdclem2  10525  iundom2g  10551  uniimadom  10555  cardmin  10575  alephval2  10584  alephreg  10594  fpwwe2lem11  10653  wunex2  10750  wuncval2  10759  tskwe2  10785  inar1  10787  tskuni  10795  gruun  10818  intgru  10826  grutsk1  10833  genpcl  11020  ltexprlem5  11052  suplem1pr  11064  supexpr  11066  supsrlem  11123  axpre-sup  11181  negfi  12191  supaddc  12209  supadd  12210  supmul1  12211  supmullem1  12212  supmul  12214  peano5nni  12263  uzind  12716  zindd  12725  uzwo  12963  lbzbi  12988  xrsupsslem  13361  xrinfmsslem  13362  supxrun  13370  supxrpnf  13372  supxrunb1  13373  supxrunb2  13374  icoshftf1o  13529  flval3  13878  axdc4uzlem  14049  tpfo  14567  wrdnfi  14615  ccatrn  14657  ccatalpha  14662  2cshw  14886  cshweqrep  14894  s3iunsndisj  15043  rtrclreclem4  15136  dfrtrcl2  15137  01sqrexlem1  15331  01sqrexlem6  15336  fsum0diag2  15871  alzdvds  16414  gcdcllem1  16593  lcmfunsnlem2lem1  16732  lcmfunsnlem2lem2  16733  maxprmfct  16804  hashgcdeq  16885  unbenlem  17004  vdwlem6  17082  vdwlem10  17086  firest  17521  mrieqv2d  17731  iscatd  17765  initoeu2  18109  setcmon  18180  setcepi  18181  fullestrcsetc  18243  fullsetcestrc  18258  isglbd  18601  isacs4lem  18636  acsfiindd  18645  acsmapd  18646  psss  18672  mgmn0plusgf  18745  sgrpidmnd  18843  pwmnd  19057  ghmrn  19357  ghmpreima  19366  cntz2ss  19463  symgextres  19553  psgnunilem2  19623  lsmsubg  19782  efgsfo  19867  gsumzaddlem  20049  gsummptnn0fzfv  20115  dmdprdd  20129  dprd2da  20172  ablsimpgprmd  20245  imasring  20472  01eq0ring  20692  isabvd  20979  issrngd  21022  islssd  21120  lbsextlem3  21348  lbsextlem4  21349  unichnlidl  21426  lidldvgen  21566  pzriprnglem4  21698  pzriprnglem7  21701  pzriprnglem13  21707  psgnghm  21794  isphld  21868  frlmsslsp  22010  mp2pm2mplem4  23035  tgcl  23195  distop  23221  indistopon  23227  pptbas  23234  toponmre  23319  opnnei  23346  neiuni  23348  neindisj2  23349  ordtrest2  23430  cnpnei  23490  cnindis  23518  cmpcld  23628  uncmp  23629  hauscmplem  23632  2ndc1stc  23677  1stcrest  23679  1stcelcls  23688  llyrest  23712  nllyrest  23713  cldllycmp  23722  reftr  23741  locfincf  23758  comppfsc  23759  txcls  23831  ptpjcn  23838  ptclsg  23842  dfac14lem  23844  xkoccn  23846  txlly  23863  txnlly  23864  ptrescn  23866  tx1stc  23877  xkoco1cn  23884  xkoco2cn  23885  xkococn  23887  xkoinjcn  23914  qtopeu  23943  hmeofval  23985  ordthmeolem  24028  isfild  24085  fbasrn  24111  trfil2  24114  flimclslem  24211  fclsrest  24251  fclscf  24252  flimfcls  24253  alexsubALTlem1  24274  alexsubALTlem2  24275  alexsubALTlem3  24276  alexsubALT  24278  qustgpopn  24347  isxmetd  24553  imasdsf1olem  24600  blcls  24733  prdsxmslem2  24756  metustfbas  24784  dscmet  24799  nrmmetd  24801  reperflem  25046  reconnlem2  25055  xrge0tsms  25062  fsumcn  25099  cnheibor  25184  tcphcph  25466  lmmbr  25487  caubl  25537  ivthlem1  25680  ovolctb  25719  ovoliunlem2  25732  ovolscalem1  25742  ovolicc2  25751  voliunlem3  25781  ismbfd  25868  mbfimaopnlem  25884  itg2le  25968  ellimc2  26106  c1liplem1  26225  plyeq0lem  26437  dgreq0  26492  aannenlem1  26561  pilem2  26685  cxpcn3lem  26982  scvxcvx  27220  musum  27425  fsumdvdsmul  27429  dchrisum0flb  27744  ostth2lem2  27868  ltsval2  27890  nolesgn2ores  27906  nogesgn1ores  27908  nosupres  27941  nosupbnd2lem1  27949  noinfres  27956  noinfbnd2lem1  27964  cutsun12  28053  madebdayim  28151  precsexlem9  28478  addonbday  28542  noseqind  28555  z12zsodd  28745  numedglnl  29587  upgrreslem  29750  umgrreslem  29751  nbuhgr  29789  nbumgr  29793  uhgrnbgr0nb  29800  nbusgrf1o0  29815  uvtxnbgrvtx  29839  cusgrfilem2  29902  uspgr2wlkeq  30091  subgrwlk  30134  wwlks  30289  iswwlksnon  30307  rusgr0edg  30430  clwwlkccatlem  30445  clwwisshclwwslem  30470  clwwlkn  30482  clwwlknon  30546  3cyclfrgrrn  30752  vdgn1frgrv3  30763  2wspmdisj  30803  numclwlk2lem2f1o  30845  frgrregord013  30861  htthlem  31384  ocsh  31750  shintcli  31796  pjss2coi  32631  pjnormssi  32635  pjclem4  32666  pj3si  32674  pj3cor1i  32676  strlem3a  32719  strb  32725  hstrlem3a  32727  hstrbi  32733  spansncv2  32760  mdsl1i  32788  cvmdi  32791  mdexchi  32802  h1da  32816  mdsymlem6  32875  sumdmdii  32882  dmdbr5ati  32889  isoun  33161  xrge0tsmsd  33500  ordtrest2NEW  34420  pwsiga  34627  measiun  34716  dya2iocuni  34781  bnj518  35382  bnj1137  35491  bnj1136  35493  bnj1413  35531  bnj1417  35537  bnj60  35558  rankval4b  35594  r1filim  35599  trssfir1om  35608  fineqvnttrclselem3  35636  fineqvinfep  35638  tz9.1regs  35647  trssfir1omregs  35649  gblacfnacd  35686  onvf1odlem1  35687  onvf1odlem4  35690  vonf1oonfo  35699  erdszelem8  35764  cvmsss2  35840  cvmfolem  35845  fmlasucdisj  35965  satfun  35977  dfon2lem8  36354  dfon2lem9  36355  dfon2  36356  rdgprc  36358  nn0prpwlem  36928  ntruni  36933  clsint2  36935  fneint  36954  fnessref  36963  refssfne  36964  neibastop1  36965  neibastop2lem  36966  mh-inf3f1  37147  bj-0int  37838  bj-ismooredr  37846  relowlpssretop  38105  fvineqsneu  38152  fvineqsneq  38153  heicant  38391  mblfinlem1  38393  ftc2nc  38438  sdclem2  38479  fdc  38482  seqpo  38484  prdsbnd  38530  heibor  38558  rrnequiv  38572  0idl  38762  intidl  38766  unichnidl  38768  prnc  38804  refressn  39268  lsmcv2  39889  lcvexchlem4  39897  lcvexchlem5  39898  eqlkr  39959  paddclN  40702  pclfinN  40760  ldilcnv  40975  ldilco  40976  cdleme25dN  41216  cdlemj2  41682  tendocan  41684  erng1lem  41847  erngdvlem4-rN  41859  dihord2pre  42085  dihglblem2N  42154  dochvalr  42217  hdmap14lem12  42739  hdmap14lem13  42740  supinf  43096  fsuppind  43423  pellfundre  43709  pellfundge  43710  pellfundlb  43712  dford3lem1  43854  aomclem2  43883  oaabsb  44122  cantnf2  44153  ofoafg  44182  naddcnff  44190  naddwordnexlem3  44227  naddwordnexlem4  44229  pwinfi3  44390  iunrelexp0  44529  iunrelexpmin1  44535  iunrelexpmin2  44539  dftrcl3  44547  cnvtrclfv  44551  trclimalb2  44553  dfrtrcl3  44560  ntrneiel2  44913  ntrneik4w  44927  ntrrn  44949  gneispa  44957  gneispb  44958  addrcom  45284  iunconnlem2  45744  ssuzfz  46166  dvnprodlem3  46763  funressnfv  47918  cfsetsnfsetfo  47935  tz6.12-afv  48048  tz6.12-afv2  48115  otiunsndisjX  48154  uniimaprimaeqfv  48269  iccpartltu  48312  iccpartgtl  48313  iccpartleu  48315  iccpartgel  48316  fargshiftf  48327  fargshiftfva  48330  sbgoldbst  48681  bgoldbtbnd  48712  tgblthelfgott  48718  grimuhgr  48790  grimco  48792  isuspgrim0  48797  isuspgrimlem  48798  upgrimpths  48812  gricushgr  48820  grtriclwlk3  48848  stgr0  48863  uspgrlim  48895  grlicsym  48916  nnsgrp  49079  ellcoellss  49352  lindsrng01  49385  suppdm  49427  nn0sumshdiglem1  49538  setrec2fun  50605