Theorem ralrimiv 3145

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ral 3062

This theorem is referenced by:  ralrimiva  3146  ralrimivw  3150  ralrimdv  3152  reximdvaiOLD  3166  ralrimivv  3198  raleleqOLD  3340  rr19.3v  3657  class2seteq  3700  rabssdv  4072  rzalALT  4509  disjord  5136  disjiund  5138  trin  5277  ralxfrALT  5413  otiunsndisj  5520  onmindif  6456  fnprb  7212  fntpb  7213  f1cdmsn  7282  ssorduni  7768  onminex  7792  onmindif2  7797  sucexeloniOLD  7800  suceloniOLD  7802  limuni3  7843  frxp  8114  poxp  8116  sexp2  8134  sexp3  8141  wfrlem15OLD  8325  onfununi  8343  onnseq  8346  tfrlem12  8391  tz7.48-2  8444  oaass  8563  omass  8582  oelim2  8597  oelimcl  8602  oaabs2  8650  omabs  8652  undifixp  8930  dom2lem  8990  isinf  9262  isinfOLD  9263  unblem4  9300  unbnn2  9302  marypha1lem  9430  supiso  9472  ordiso2  9512  card2inf  9552  elirrv  9593  wemapwe  9694  ttrclss  9717  trcl  9725  frr3g  9753  tz9.13  9788  rankval3b  9823  rankunb  9847  rankuni2b  9850  scott0  9883  updjud  9931  dfac8alem  10026  carduniima  10093  alephsmo  10099  alephval3  10107  iunfictbso  10111  dfac3  10118  dfac5lem5  10124  dfac12r  10143  dfac12k  10144  kmlem4  10150  kmlem11  10157  cfsuc  10254  cofsmo  10266  cfsmolem  10267  coftr  10270  alephsing  10273  infpssrlem3  10302  fin23lem30  10339  isf32lem2  10351  isf32lem3  10352  isf34lem6  10377  fin1a2lem11  10407  fin1a2lem13  10409  fin1a2s  10411  axcc2lem  10433  domtriomlem  10439  axdc3lem2  10448  axdc4lem  10452  axcclem  10454  axdclem2  10517  iundom2g  10537  uniimadom  10541  cardmin  10561  alephval2  10569  alephreg  10579  fpwwe2lem11  10638  wunex2  10735  wuncval2  10744  tskwe2  10770  inar1  10772  tskuni  10780  gruun  10803  intgru  10811  grutsk1  10818  genpcl  11005  ltexprlem5  11037  suplem1pr  11049  supexpr  11051  supsrlem  11108  axpre-sup  11166  negfi  12165  supaddc  12183  supadd  12184  supmul1  12185  supmullem1  12186  supmul  12188  peano5nni  12217  uzind  12656  zindd  12665  uzwo  12897  lbzbi  12922  xrsupsslem  13288  xrinfmsslem  13289  supxrun  13297  supxrpnf  13299  supxrunb1  13300  supxrunb2  13301  icoshftf1o  13453  flval3  13782  axdc4uzlem  13950  wrdnfi  14500  ccatrn  14541  ccatalpha  14545  2cshw  14765  cshweqrep  14773  s3iunsndisj  14917  rtrclreclem4  15010  dfrtrcl2  15011  01sqrexlem1  15191  01sqrexlem6  15196  fsum0diag2  15731  alzdvds  16265  gcdcllem1  16442  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  maxprmfct  16648  hashgcdeq  16724  unbenlem  16843  vdwlem6  16921  vdwlem10  16925  firest  17380  mrieqv2d  17585  iscatd  17619  initoeu2  17968  setcmon  18039  setcepi  18040  fullestrcsetc  18105  fullsetcestrc  18120  isglbd  18464  isacs4lem  18499  acsfiindd  18508  acsmapd  18509  psss  18535  sgrpidmnd  18632  pwmnd  18820  ghmrn  19107  ghmpreima  19116  cntz2ss  19201  symgextres  19295  psgnunilem2  19365  lsmsubg  19524  efgsfo  19609  gsumzaddlem  19791  gsummptnn0fzfv  19857  dmdprdd  19871  dprd2da  19914  ablsimpgprmd  19987  imasring  20147  01eq0ring  20309  isabvd  20432  issrngd  20473  islssd  20551  lbsextlem3  20779  lbsextlem4  20780  lidldvgen  20899  psgnghm  21139  isphld  21213  frlmsslsp  21357  mp2pm2mplem4  22318  tgcl  22479  distop  22505  indistopon  22511  pptbas  22518  toponmre  22604  opnnei  22631  neiuni  22633  neindisj2  22634  ordtrest2  22715  cnpnei  22775  cnindis  22803  cmpcld  22913  uncmp  22914  hauscmplem  22917  2ndc1stc  22962  1stcrest  22964  1stcelcls  22972  llyrest  22996  nllyrest  22997  cldllycmp  23006  reftr  23025  locfincf  23042  comppfsc  23043  txcls  23115  ptpjcn  23122  ptclsg  23126  dfac14lem  23128  xkoccn  23130  txlly  23147  txnlly  23148  ptrescn  23150  tx1stc  23161  xkoco1cn  23168  xkoco2cn  23169  xkococn  23171  xkoinjcn  23198  qtopeu  23227  hmeofval  23269  ordthmeolem  23312  isfild  23369  fbasrn  23395  trfil2  23398  flimclslem  23495  fclsrest  23535  fclscf  23536  flimfcls  23537  alexsubALTlem1  23558  alexsubALTlem2  23559  alexsubALTlem3  23560  alexsubALT  23562  qustgpopn  23631  isxmetd  23839  imasdsf1olem  23886  blcls  24022  prdsxmslem2  24045  metustfbas  24073  dscmet  24088  nrmmetd  24090  reperflem  24341  reconnlem2  24350  xrge0tsms  24357  fsumcn  24393  cnheibor  24478  tcphcph  24761  lmmbr  24782  caubl  24832  ivthlem1  24975  ovolctb  25014  ovoliunlem2  25027  ovolscalem1  25037  ovolicc2  25046  voliunlem3  25076  ismbfd  25163  mbfimaopnlem  25179  itg2le  25264  ellimc2  25401  c1liplem1  25520  plyeq0lem  25731  dgreq0  25786  aannenlem1  25848  pilem2  25971  cxpcn3lem  26262  scvxcvx  26497  musum  26702  dchrisum0flb  27020  ostth2lem2  27144  sltval2  27166  nolesgn2ores  27182  nogesgn1ores  27184  nosupres  27217  nosupbnd2lem1  27225  noinfres  27232  noinfbnd2lem1  27240  scutun12  27319  madebdayim  27390  precsexlem9  27671  peano5n0s  27706  numedglnl  28442  upgrreslem  28599  umgrreslem  28600  nbuhgr  28638  nbumgr  28642  uhgrnbgr0nb  28649  nbusgrf1o0  28664  uvtxnbgrvtx  28688  cusgrfilem2  28751  uspgr2wlkeq  28941  wwlks  29127  iswwlksnon  29145  rusgr0edg  29265  clwwlkccatlem  29280  clwwisshclwwslem  29305  clwwlkn  29317  clwwlknon  29381  3cyclfrgrrn  29577  vdgn1frgrv3  29588  2wspmdisj  29628  numclwlk2lem2f1o  29670  frgrregord013  29686  htthlem  30208  ocsh  30574  shintcli  30620  pjss2coi  31455  pjnormssi  31459  pjclem4  31490  pj3si  31498  pj3cor1i  31500  strlem3a  31543  strb  31549  hstrlem3a  31551  hstrbi  31557  spansncv2  31584  mdsl1i  31612  cvmdi  31615  mdexchi  31626  h1da  31640  mdsymlem6  31699  sumdmdii  31706  dmdbr5ati  31713  isoun  31961  supssd  31972  infssd  31973  xrge0tsmsd  32250  ordtrest2NEW  32972  pwsiga  33197  measiun  33285  dya2iocuni  33351  bnj518  33966  bnj1137  34075  bnj1136  34077  bnj1413  34115  bnj1417  34121  bnj60  34142  subgrwlk  34192  erdszelem8  34258  cvmsss2  34334  cvmfolem  34339  fmlasucdisj  34459  satfun  34471  dfon2lem8  34831  dfon2lem9  34832  dfon2  34833  rdgprc  34835  nn0prpwlem  35293  ntruni  35298  clsint2  35300  fneint  35319  fnessref  35328  refssfne  35329  neibastop1  35330  neibastop2lem  35331  bj-0int  36068  bj-ismooredr  36076  relowlpssretop  36331  fvineqsneu  36378  fvineqsneq  36379  heicant  36609  mblfinlem1  36611  ftc2nc  36656  sdclem2  36696  fdc  36699  seqpo  36701  prdsbnd  36747  heibor  36775  rrnequiv  36789  0idl  36979  intidl  36983  unichnidl  36985  prnc  37021  uniqsALTV  37284  refressn  37399  lsmcv2  37985  lcvexchlem4  37993  lcvexchlem5  37994  eqlkr  38055  paddclN  38799  pclfinN  38857  ldilcnv  39072  ldilco  39073  cdleme25dN  39313  cdlemj2  39779  tendocan  39781  erng1lem  39944  erngdvlem4-rN  39956  dihord2pre  40182  dihglblem2N  40251  dochvalr  40314  hdmap14lem12  40836  hdmap14lem13  40837  fsuppind  41244  pellfundre  41701  pellfundge  41702  pellfundlb  41704  dford3lem1  41847  aomclem2  41879  oaabsb  42126  cantnf2  42157  ofoafg  42186  naddcnff  42194  naddwordnexlem3  42232  naddwordnexlem4  42234  pwinfi3  42396  iunrelexp0  42535  iunrelexpmin1  42541  iunrelexpmin2  42545  dftrcl3  42553  cnvtrclfv  42557  trclimalb2  42559  dfrtrcl3  42566  ntrneiel2  42919  ntrneik4w  42933  ntrrn  42955  gneispa  42963  gneispb  42964  addrcom  43316  iunconnlem2  43778  ssuzfz  44138  dvmptfprod  44740  dvnprodlem3  44743  funressnfv  45832  cfsetsnfsetfo  45849  tz6.12-afv  45960  tz6.12-afv2  46027  otiunsndisjX  46066  uniimaprimaeqfv  46129  iccpartltu  46172  iccpartgtl  46173  iccpartleu  46175  iccpartgel  46176  fargshiftf  46187  fargshiftfva  46190  sbgoldbst  46525  bgoldbtbnd  46556  tgblthelfgott  46562  isomushgr  46573  nnsgrp  46666  pzriprnglem4  46887  pzriprnglem7  46890  pzriprnglem13  46896  ellcoellss  47194  lindsrng01  47227  suppdm  47269  nn0sumshdiglem1  47385  setrec2fun  47815