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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimiva  3133  ralrimivw  3137  ralrimdv  3139  ralrimivv  3186  rr19.3v  3651  class2seteq  3692  rabssdv  4055  rzalALT  4490  disjord  5113  disjiund  5115  trin  5246  ralxfrALT  5390  otiunsndisj  5500  onmindif  6451  fnprb  7205  fntpb  7206  f1cdmsn  7280  ssorduni  7778  onminex  7801  onmindif2  7806  sucexeloniOLD  7809  suceloniOLD  7811  limuni3  7852  frxp  8130  poxp  8132  sexp2  8150  sexp3  8157  wfrlem15OLD  8342  onfununi  8360  onnseq  8363  tfrlem12  8408  tz7.48-2  8461  oaass  8578  omass  8597  oelim2  8612  oelimcl  8617  oaabs2  8666  omabs  8668  undifixp  8953  dom2lem  9011  isinf  9273  isinfOLD  9274  unblem4  9308  unbnn2  9310  marypha1lem  9450  supssd  9480  supiso  9493  infssd  9511  ordiso2  9534  card2inf  9574  elirrv  9615  wemapwe  9716  ttrclss  9739  trcl  9747  frr3g  9775  tz9.13  9810  rankval3b  9845  rankunb  9869  rankuni2b  9872  scott0  9905  updjud  9953  dfac8alem  10048  carduniima  10115  alephsmo  10121  alephval3  10129  iunfictbso  10133  dfac3  10140  dfac5lem5  10146  dfac12r  10166  dfac12k  10167  kmlem4  10173  kmlem11  10180  cfsuc  10276  cofsmo  10288  cfsmolem  10289  coftr  10292  alephsing  10295  infpssrlem3  10324  fin23lem30  10361  isf32lem2  10373  isf32lem3  10374  isf34lem6  10399  fin1a2lem11  10429  fin1a2lem13  10431  fin1a2s  10433  axcc2lem  10455  domtriomlem  10461  axdc3lem2  10470  axdc4lem  10474  axcclem  10476  axdclem2  10539  iundom2g  10559  uniimadom  10563  cardmin  10583  alephval2  10591  alephreg  10601  fpwwe2lem11  10660  wunex2  10757  wuncval2  10766  tskwe2  10792  inar1  10794  tskuni  10802  gruun  10825  intgru  10833  grutsk1  10840  genpcl  11027  ltexprlem5  11059  suplem1pr  11071  supexpr  11073  supsrlem  11130  axpre-sup  11188  negfi  12196  supaddc  12214  supadd  12215  supmul1  12216  supmullem1  12217  supmul  12219  peano5nni  12248  uzind  12690  zindd  12699  uzwo  12932  lbzbi  12957  xrsupsslem  13328  xrinfmsslem  13329  supxrun  13337  supxrpnf  13339  supxrunb1  13340  supxrunb2  13341  icoshftf1o  13496  flval3  13837  axdc4uzlem  14006  tpfo  14523  wrdnfi  14571  ccatrn  14612  ccatalpha  14616  2cshw  14836  cshweqrep  14844  s3iunsndisj  14992  rtrclreclem4  15085  dfrtrcl2  15086  01sqrexlem1  15266  01sqrexlem6  15271  fsum0diag2  15804  alzdvds  16344  gcdcllem1  16523  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  maxprmfct  16733  hashgcdeq  16814  unbenlem  16933  vdwlem6  17011  vdwlem10  17015  firest  17451  mrieqv2d  17656  iscatd  17690  initoeu2  18034  setcmon  18105  setcepi  18106  fullestrcsetc  18168  fullsetcestrc  18183  isglbd  18524  isacs4lem  18559  acsfiindd  18568  acsmapd  18569  psss  18595  sgrpidmnd  18722  pwmnd  18920  ghmrn  19217  ghmpreima  19226  cntz2ss  19323  symgextres  19411  psgnunilem2  19481  lsmsubg  19640  efgsfo  19725  gsumzaddlem  19907  gsummptnn0fzfv  19973  dmdprdd  19987  dprd2da  20030  ablsimpgprmd  20103  imasring  20295  01eq0ring  20495  isabvd  20777  issrngd  20820  islssd  20897  lbsextlem3  21126  lbsextlem4  21127  lidldvgen  21300  pzriprnglem4  21450  pzriprnglem7  21453  pzriprnglem13  21459  psgnghm  21545  isphld  21619  frlmsslsp  21761  mp2pm2mplem4  22752  tgcl  22912  distop  22938  indistopon  22944  pptbas  22951  toponmre  23036  opnnei  23063  neiuni  23065  neindisj2  23066  ordtrest2  23147  cnpnei  23207  cnindis  23235  cmpcld  23345  uncmp  23346  hauscmplem  23349  2ndc1stc  23394  1stcrest  23396  1stcelcls  23404  llyrest  23428  nllyrest  23429  cldllycmp  23438  reftr  23457  locfincf  23474  comppfsc  23475  txcls  23547  ptpjcn  23554  ptclsg  23558  dfac14lem  23560  xkoccn  23562  txlly  23579  txnlly  23580  ptrescn  23582  tx1stc  23593  xkoco1cn  23600  xkoco2cn  23601  xkococn  23603  xkoinjcn  23630  qtopeu  23659  hmeofval  23701  ordthmeolem  23744  isfild  23801  fbasrn  23827  trfil2  23830  flimclslem  23927  fclsrest  23967  fclscf  23968  flimfcls  23969  alexsubALTlem1  23990  alexsubALTlem2  23991  alexsubALTlem3  23992  alexsubALT  23994  qustgpopn  24063  isxmetd  24270  imasdsf1olem  24317  blcls  24450  prdsxmslem2  24473  metustfbas  24501  dscmet  24516  nrmmetd  24518  reperflem  24763  reconnlem2  24772  xrge0tsms  24779  fsumcn  24817  cnheibor  24910  tcphcph  25194  lmmbr  25215  caubl  25265  ivthlem1  25409  ovolctb  25448  ovoliunlem2  25461  ovolscalem1  25471  ovolicc2  25480  voliunlem3  25510  ismbfd  25597  mbfimaopnlem  25613  itg2le  25697  ellimc2  25835  c1liplem1  25958  plyeq0lem  26172  dgreq0  26228  aannenlem1  26293  pilem2  26419  cxpcn3lem  26714  scvxcvx  26953  musum  27158  fsumdvdsmul  27162  dchrisum0flb  27478  ostth2lem2  27602  sltval2  27625  nolesgn2ores  27641  nogesgn1ores  27643  nosupres  27676  nosupbnd2lem1  27684  noinfres  27691  noinfbnd2lem1  27699  scutun12  27779  madebdayim  27856  precsexlem9  28174  noseqind  28243  zs12bday  28400  numedglnl  29128  upgrreslem  29288  umgrreslem  29289  nbuhgr  29327  nbumgr  29331  uhgrnbgr0nb  29338  nbusgrf1o0  29353  uvtxnbgrvtx  29377  cusgrfilem2  29441  uspgr2wlkeq  29631  wwlks  29822  iswwlksnon  29840  rusgr0edg  29960  clwwlkccatlem  29975  clwwisshclwwslem  30000  clwwlkn  30012  clwwlknon  30076  3cyclfrgrrn  30272  vdgn1frgrv3  30283  2wspmdisj  30323  numclwlk2lem2f1o  30365  frgrregord013  30381  htthlem  30903  ocsh  31269  shintcli  31315  pjss2coi  32150  pjnormssi  32154  pjclem4  32185  pj3si  32193  pj3cor1i  32195  strlem3a  32238  strb  32244  hstrlem3a  32246  hstrbi  32252  spansncv2  32279  mdsl1i  32307  cvmdi  32310  mdexchi  32321  h1da  32335  mdsymlem6  32394  sumdmdii  32401  dmdbr5ati  32408  isoun  32684  xrge0tsmsd  33061  ordtrest2NEW  33959  pwsiga  34166  measiun  34254  dya2iocuni  34320  bnj518  34922  bnj1137  35031  bnj1136  35033  bnj1413  35071  bnj1417  35077  bnj60  35098  gblacfnacd  35135  subgrwlk  35159  erdszelem8  35225  cvmsss2  35301  cvmfolem  35306  fmlasucdisj  35426  satfun  35438  dfon2lem8  35813  dfon2lem9  35814  dfon2  35815  rdgprc  35817  nn0prpwlem  36345  ntruni  36350  clsint2  36352  fneint  36371  fnessref  36380  refssfne  36381  neibastop1  36382  neibastop2lem  36383  bj-0int  37124  bj-ismooredr  37132  relowlpssretop  37387  fvineqsneu  37434  fvineqsneq  37435  heicant  37684  mblfinlem1  37686  ftc2nc  37731  sdclem2  37771  fdc  37774  seqpo  37776  prdsbnd  37822  heibor  37850  rrnequiv  37864  0idl  38054  intidl  38058  unichnidl  38060  prnc  38096  uniqsALTV  38352  refressn  38466  lsmcv2  39052  lcvexchlem4  39060  lcvexchlem5  39061  eqlkr  39122  paddclN  39866  pclfinN  39924  ldilcnv  40139  ldilco  40140  cdleme25dN  40380  cdlemj2  40846  tendocan  40848  erng1lem  41011  erngdvlem4-rN  41023  dihord2pre  41249  dihglblem2N  41318  dochvalr  41381  hdmap14lem12  41903  hdmap14lem13  41904  supinf  42260  fsuppind  42588  pellfundre  42879  pellfundge  42880  pellfundlb  42882  dford3lem1  43025  aomclem2  43054  oaabsb  43293  cantnf2  43324  ofoafg  43353  naddcnff  43361  naddwordnexlem3  43398  naddwordnexlem4  43400  pwinfi3  43562  iunrelexp0  43701  iunrelexpmin1  43707  iunrelexpmin2  43711  dftrcl3  43719  cnvtrclfv  43723  trclimalb2  43725  dfrtrcl3  43732  ntrneiel2  44085  ntrneik4w  44099  ntrrn  44121  gneispa  44129  gneispb  44130  addrcom  44474  iunconnlem2  44934  ssuzfz  45356  dvnprodlem3  45957  funressnfv  47052  cfsetsnfsetfo  47069  tz6.12-afv  47182  tz6.12-afv2  47249  otiunsndisjX  47288  uniimaprimaeqfv  47376  iccpartltu  47419  iccpartgtl  47420  iccpartleu  47422  iccpartgel  47423  fargshiftf  47434  fargshiftfva  47437  sbgoldbst  47772  bgoldbtbnd  47803  tgblthelfgott  47809  grimuhgr  47880  grimco  47882  isuspgrim0  47887  isuspgrimlem  47888  upgrimpths  47902  gricushgr  47910  grtriclwlk3  47937  stgr0  47952  uspgrlim  47984  grlicsym  47998  nnsgrp  48132  ellcoellss  48391  lindsrng01  48424  suppdm  48466  nn0sumshdiglem1  48581  setrec2fun  49536