Theorem ralrimiv 3143

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  ralrimiva  3144  ralrimivw  3148  ralrimdv  3150  reximdvaiOLD  3164  ralrimivv  3198  rr19.3v  3667  class2seteq  3713  rabssdv  4085  rzalALT  4516  disjord  5137  disjiund  5139  trin  5277  ralxfrALT  5421  otiunsndisj  5530  onmindif  6478  fnprb  7228  fntpb  7229  f1cdmsn  7302  ssorduni  7798  onminex  7822  onmindif2  7827  sucexeloniOLD  7830  suceloniOLD  7832  limuni3  7873  frxp  8150  poxp  8152  sexp2  8170  sexp3  8177  wfrlem15OLD  8362  onfununi  8380  onnseq  8383  tfrlem12  8428  tz7.48-2  8481  oaass  8598  omass  8617  oelim2  8632  oelimcl  8637  oaabs2  8686  omabs  8688  undifixp  8973  dom2lem  9031  isinf  9294  isinfOLD  9295  unblem4  9329  unbnn2  9331  marypha1lem  9471  supiso  9513  ordiso2  9553  card2inf  9593  elirrv  9634  wemapwe  9735  ttrclss  9758  trcl  9766  frr3g  9794  tz9.13  9829  rankval3b  9864  rankunb  9888  rankuni2b  9891  scott0  9924  updjud  9972  dfac8alem  10067  carduniima  10134  alephsmo  10140  alephval3  10148  iunfictbso  10152  dfac3  10159  dfac5lem5  10165  dfac12r  10185  dfac12k  10186  kmlem4  10192  kmlem11  10199  cfsuc  10295  cofsmo  10307  cfsmolem  10308  coftr  10311  alephsing  10314  infpssrlem3  10343  fin23lem30  10380  isf32lem2  10392  isf32lem3  10393  isf34lem6  10418  fin1a2lem11  10448  fin1a2lem13  10450  fin1a2s  10452  axcc2lem  10474  domtriomlem  10480  axdc3lem2  10489  axdc4lem  10493  axcclem  10495  axdclem2  10558  iundom2g  10578  uniimadom  10582  cardmin  10602  alephval2  10610  alephreg  10620  fpwwe2lem11  10679  wunex2  10776  wuncval2  10785  tskwe2  10811  inar1  10813  tskuni  10821  gruun  10844  intgru  10852  grutsk1  10859  genpcl  11046  ltexprlem5  11078  suplem1pr  11090  supexpr  11092  supsrlem  11149  axpre-sup  11207  negfi  12215  supaddc  12233  supadd  12234  supmul1  12235  supmullem1  12236  supmul  12238  peano5nni  12267  uzind  12708  zindd  12717  uzwo  12951  lbzbi  12976  xrsupsslem  13346  xrinfmsslem  13347  supxrun  13355  supxrpnf  13357  supxrunb1  13358  supxrunb2  13359  icoshftf1o  13511  flval3  13852  axdc4uzlem  14021  tpfo  14536  wrdnfi  14583  ccatrn  14624  ccatalpha  14628  2cshw  14848  cshweqrep  14856  s3iunsndisj  15004  rtrclreclem4  15097  dfrtrcl2  15098  01sqrexlem1  15278  01sqrexlem6  15283  fsum0diag2  15816  alzdvds  16354  gcdcllem1  16533  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  maxprmfct  16743  hashgcdeq  16823  unbenlem  16942  vdwlem6  17020  vdwlem10  17024  firest  17479  mrieqv2d  17684  iscatd  17718  initoeu2  18070  setcmon  18141  setcepi  18142  fullestrcsetc  18207  fullsetcestrc  18222  isglbd  18567  isacs4lem  18602  acsfiindd  18611  acsmapd  18612  psss  18638  sgrpidmnd  18765  pwmnd  18963  ghmrn  19260  ghmpreima  19269  cntz2ss  19366  symgextres  19458  psgnunilem2  19528  lsmsubg  19687  efgsfo  19772  gsumzaddlem  19954  gsummptnn0fzfv  20020  dmdprdd  20034  dprd2da  20077  ablsimpgprmd  20150  imasring  20344  01eq0ring  20547  isabvd  20830  issrngd  20873  islssd  20951  lbsextlem3  21180  lbsextlem4  21181  lidldvgen  21362  pzriprnglem4  21513  pzriprnglem7  21516  pzriprnglem13  21522  psgnghm  21616  isphld  21690  frlmsslsp  21834  mp2pm2mplem4  22831  tgcl  22992  distop  23018  indistopon  23024  pptbas  23031  toponmre  23117  opnnei  23144  neiuni  23146  neindisj2  23147  ordtrest2  23228  cnpnei  23288  cnindis  23316  cmpcld  23426  uncmp  23427  hauscmplem  23430  2ndc1stc  23475  1stcrest  23477  1stcelcls  23485  llyrest  23509  nllyrest  23510  cldllycmp  23519  reftr  23538  locfincf  23555  comppfsc  23556  txcls  23628  ptpjcn  23635  ptclsg  23639  dfac14lem  23641  xkoccn  23643  txlly  23660  txnlly  23661  ptrescn  23663  tx1stc  23674  xkoco1cn  23681  xkoco2cn  23682  xkococn  23684  xkoinjcn  23711  qtopeu  23740  hmeofval  23782  ordthmeolem  23825  isfild  23882  fbasrn  23908  trfil2  23911  flimclslem  24008  fclsrest  24048  fclscf  24049  flimfcls  24050  alexsubALTlem1  24071  alexsubALTlem2  24072  alexsubALTlem3  24073  alexsubALT  24075  qustgpopn  24144  isxmetd  24352  imasdsf1olem  24399  blcls  24535  prdsxmslem2  24558  metustfbas  24586  dscmet  24601  nrmmetd  24603  reperflem  24854  reconnlem2  24863  xrge0tsms  24870  fsumcn  24908  cnheibor  25001  tcphcph  25285  lmmbr  25306  caubl  25356  ivthlem1  25500  ovolctb  25539  ovoliunlem2  25552  ovolscalem1  25562  ovolicc2  25571  voliunlem3  25601  ismbfd  25688  mbfimaopnlem  25704  itg2le  25789  ellimc2  25927  c1liplem1  26050  plyeq0lem  26264  dgreq0  26320  aannenlem1  26385  pilem2  26511  cxpcn3lem  26805  scvxcvx  27044  musum  27249  fsumdvdsmul  27253  dchrisum0flb  27569  ostth2lem2  27693  sltval2  27716  nolesgn2ores  27732  nogesgn1ores  27734  nosupres  27767  nosupbnd2lem1  27775  noinfres  27782  noinfbnd2lem1  27790  scutun12  27870  madebdayim  27941  precsexlem9  28254  noseqind  28313  zs12bday  28439  numedglnl  29176  upgrreslem  29336  umgrreslem  29337  nbuhgr  29375  nbumgr  29379  uhgrnbgr0nb  29386  nbusgrf1o0  29401  uvtxnbgrvtx  29425  cusgrfilem2  29489  uspgr2wlkeq  29679  wwlks  29865  iswwlksnon  29883  rusgr0edg  30003  clwwlkccatlem  30018  clwwisshclwwslem  30043  clwwlkn  30055  clwwlknon  30119  3cyclfrgrrn  30315  vdgn1frgrv3  30326  2wspmdisj  30366  numclwlk2lem2f1o  30408  frgrregord013  30424  htthlem  30946  ocsh  31312  shintcli  31358  pjss2coi  32193  pjnormssi  32197  pjclem4  32228  pj3si  32236  pj3cor1i  32238  strlem3a  32281  strb  32287  hstrlem3a  32289  hstrbi  32295  spansncv2  32322  mdsl1i  32350  cvmdi  32353  mdexchi  32364  h1da  32378  mdsymlem6  32437  sumdmdii  32444  dmdbr5ati  32451  isoun  32717  supssd  32727  infssd  32728  xrge0tsmsd  33048  ordtrest2NEW  33884  pwsiga  34111  measiun  34199  dya2iocuni  34265  bnj518  34879  bnj1137  34988  bnj1136  34990  bnj1413  35028  bnj1417  35034  bnj60  35055  gblacfnacd  35092  subgrwlk  35117  erdszelem8  35183  cvmsss2  35259  cvmfolem  35264  fmlasucdisj  35384  satfun  35396  dfon2lem8  35772  dfon2lem9  35773  dfon2  35774  rdgprc  35776  nn0prpwlem  36305  ntruni  36310  clsint2  36312  fneint  36331  fnessref  36340  refssfne  36341  neibastop1  36342  neibastop2lem  36343  bj-0int  37084  bj-ismooredr  37092  relowlpssretop  37347  fvineqsneu  37394  fvineqsneq  37395  heicant  37642  mblfinlem1  37644  ftc2nc  37689  sdclem2  37729  fdc  37732  seqpo  37734  prdsbnd  37780  heibor  37808  rrnequiv  37822  0idl  38012  intidl  38016  unichnidl  38018  prnc  38054  uniqsALTV  38311  refressn  38425  lsmcv2  39011  lcvexchlem4  39019  lcvexchlem5  39020  eqlkr  39081  paddclN  39825  pclfinN  39883  ldilcnv  40098  ldilco  40099  cdleme25dN  40339  cdlemj2  40805  tendocan  40807  erng1lem  40970  erngdvlem4-rN  40982  dihord2pre  41208  dihglblem2N  41277  dochvalr  41340  hdmap14lem12  41862  hdmap14lem13  41863  supinf  42262  fsuppind  42577  pellfundre  42869  pellfundge  42870  pellfundlb  42872  dford3lem1  43015  aomclem2  43044  oaabsb  43284  cantnf2  43315  ofoafg  43344  naddcnff  43352  naddwordnexlem3  43389  naddwordnexlem4  43391  pwinfi3  43553  iunrelexp0  43692  iunrelexpmin1  43698  iunrelexpmin2  43702  dftrcl3  43710  cnvtrclfv  43714  trclimalb2  43716  dfrtrcl3  43723  ntrneiel2  44076  ntrneik4w  44090  ntrrn  44112  gneispa  44120  gneispb  44121  addrcom  44471  iunconnlem2  44933  ssuzfz  45299  dvnprodlem3  45904  funressnfv  46993  cfsetsnfsetfo  47010  tz6.12-afv  47123  tz6.12-afv2  47190  otiunsndisjX  47229  uniimaprimaeqfv  47307  iccpartltu  47350  iccpartgtl  47351  iccpartleu  47353  iccpartgel  47354  fargshiftf  47365  fargshiftfva  47368  sbgoldbst  47703  bgoldbtbnd  47734  tgblthelfgott  47740  isuspgrim0  47810  isuspgrimlem  47812  grimuhgr  47816  grimco  47818  gricushgr  47824  grtriclwlk3  47850  stgr0  47863  uspgrlim  47895  grlicsym  47909  nnsgrp  48021  ellcoellss  48281  lindsrng01  48314  suppdm  48356  nn0sumshdiglem1  48471  setrec2fun  48923