Theorem ralrimiv 3164

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

Syntax hints:   → wi 4   ∈ wcel 2157  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001

This theorem depends on definitions:  df-bi 198  df-ral 3112

This theorem is referenced by:  ralrimiva  3165  ralrimivw  3166  ralrimdv  3167  ralrimivv  3169  reximdvai  3213  r19.27v  3269  raleleq  3356  rr19.3v  3551  rabssdv  3890  rzal  4279  ssdifsnOLD  4521  disjord  4844  disjiund  4846  trin  4967  class2seteq  5038  ralxfrALT  5097  otiunsndisj  5188  idrefOLD  5733  onmindif  6039  fnprb  6706  fntpb  6707  ssorduni  7224  onminex  7246  onmindif2  7251  suceloni  7252  limuni3  7291  frxp  7530  poxp  7532  wfrlem15  7674  onfununi  7683  onnseq  7686  tfrlem12  7730  tz7.48-2  7782  oaass  7887  omass  7906  oelim2  7921  oelimcl  7926  oaabs2  7971  omabs  7973  undifixp  8190  dom2lem  8241  isinf  8421  unblem4  8463  unbnn2  8465  marypha1lem  8587  supiso  8629  ordiso2  8668  card2inf  8708  elirrv  8749  wemapwe  8850  trcl  8860  tz9.13  8910  rankval3b  8945  rankunb  8969  rankuni2b  8972  scott0  9005  updjud  9052  dfac8alem  9144  carduniima  9211  alephsmo  9217  alephval3  9225  iunfictbso  9229  dfac3  9236  dfac5lem5  9242  dfac12r  9262  dfac12k  9263  kmlem4  9269  kmlem11  9276  cfsuc  9373  cofsmo  9385  cfsmolem  9386  coftr  9389  alephsing  9392  infpssrlem3  9421  fin23lem30  9458  isf32lem2  9470  isf32lem3  9471  isf34lem6  9496  fin1a2lem11  9526  fin1a2lem13  9528  fin1a2s  9530  axcc2lem  9552  domtriomlem  9558  axdc3lem2  9567  axdc4lem  9571  axcclem  9573  axdclem2  9636  iundom2g  9656  uniimadom  9660  cardmin  9680  alephval2  9688  alephreg  9698  fpwwe2lem12  9757  wunex2  9854  wuncval2  9863  tskwe2  9889  inar1  9891  tskuni  9899  gruun  9922  intgru  9930  grutsk1  9937  genpcl  10124  ltexprlem5  10156  suplem1pr  10168  supexpr  10170  supsrlem  10226  axpre-sup  10284  fiminre  11266  supaddc  11284  supadd  11285  supmul1  11286  supmullem1  11287  supmul  11289  peano5nni  11317  uzind  11754  zindd  11763  uzwo  11989  lbzbi  12014  xrsupsslem  12374  xrinfmsslem  12375  supxrun  12383  supxrpnf  12385  supxrunb1  12386  supxrunb2  12387  icoshftf1o  12535  flval3  12859  axdc4uzlem  13025  ccatrn  13605  2cshw  13802  cshweqrep  13810  s3iunsndisj  13951  rtrclreclem4  14043  dfrtrcl2  14044  sqrlem1  14225  sqrlem6  14230  fsum0diag2  14756  alzdvds  15284  gcdcllem1  15459  lcmfunsnlem2lem1  15589  lcmfunsnlem2lem2  15590  maxprmfct  15657  hashgcdeq  15730  unbenlem  15848  vdwlem6  15926  vdwlem10  15930  firest  16317  mrieqv2d  16523  iscatd  16557  setcmon  16960  setcepi  16961  fullestrcsetc  17015  fullsetcestrc  17030  isglbd  17341  isacs4lem  17392  acsfiindd  17401  acsmapd  17402  psss  17438  ghmrn  17894  ghmpreima  17903  cntz2ss  17985  symgextres  18065  psgnunilem2  18135  lsmsubg  18289  efgsfo  18372  gsumzaddlem  18541  gsummptnn0fzfv  18605  dmdprdd  18619  dprd2da  18662  imasring  18840  isabvd  19043  issrngd  19084  islssd  19159  lbsextlem3  19388  lbsextlem4  19389  lidldvgen  19483  psgnghm  20152  isphld  20228  frlmsslsp  20365  mp2pm2mplem4  20847  tgcl  21007  distop  21033  indistopon  21039  pptbas  21046  toponmre  21131  opnnei  21158  neiuni  21160  neindisj2  21161  ordtrest2  21242  cnpnei  21302  cnindis  21330  cmpcld  21439  uncmp  21440  hauscmplem  21443  2ndc1stc  21488  1stcrest  21490  1stcelcls  21498  llyrest  21522  nllyrest  21523  cldllycmp  21532  reftr  21551  locfincf  21568  comppfsc  21569  txcls  21641  ptpjcn  21648  ptclsg  21652  dfac14lem  21654  xkoccn  21656  txlly  21673  txnlly  21674  ptrescn  21676  tx1stc  21687  xkoco1cn  21694  xkoco2cn  21695  xkococn  21697  xkoinjcn  21724  qtopeu  21753  hmeofval  21795  ordthmeolem  21838  isfild  21895  fbasrn  21921  trfil2  21924  flimclslem  22021  fclsrest  22061  fclscf  22062  flimfcls  22063  alexsubALTlem1  22084  alexsubALTlem2  22085  alexsubALTlem3  22086  alexsubALT  22088  qustgpopn  22156  isxmetd  22364  imasdsf1olem  22411  blcls  22544  prdsxmslem2  22567  metustfbas  22595  dscmet  22610  nrmmetd  22612  reperflem  22854  reconnlem2  22863  xrge0tsms  22870  fsumcn  22906  cnheibor  22987  tchcph  23268  lmmbr  23289  caubl  23339  ivthlem1  23454  ovolctb  23493  ovoliunlem2  23506  ovolscalem1  23516  ovolicc2  23525  voliunlem3  23555  ismbfd  23642  mbfimaopnlem  23658  itg2le  23742  ellimc2  23877  c1liplem1  23995  plyeq0lem  24202  dgreq0  24257  aannenlem1  24319  pilem2  24442  cxpcn3lem  24724  scvxcvx  24948  musum  25153  dchrisum0flb  25435  ostth2lem2  25559  numedglnl  26276  upgrreslem  26434  umgrreslem  26435  nbuhgr  26477  nbumgr  26481  uhgrnbgr0nb  26488  nbusgrf1o0  26509  uvtxnbgrvtx  26535  cusgrfilem2  26602  uspgr2wlkeq  26792  wwlks  26978  iswwlksnon  26997  rusgr0edg  27137  clwwlkccatlem  27154  clwwisshclwwslem  27179  clwwlkn  27193  clwwlknon  27277  3cyclfrgrrn  27483  vdgn1frgrv3  27494  2wspmdisj  27534  numclwlk2lem2f1o  27581  numclwlk2lem2f1oOLD  27588  frgrregord013  27605  htthlem  28124  ocsh  28492  shintcli  28538  pjss2coi  29373  pjnormssi  29377  pjclem4  29408  pj3si  29416  pj3cor1i  29418  strlem3a  29461  strb  29467  hstrlem3a  29469  hstrbi  29475  spansncv2  29502  mdsl1i  29530  cvmdi  29533  mdexchi  29544  h1da  29558  mdsymlem6  29617  sumdmdii  29624  dmdbr5ati  29631  isoun  29828  supssd  29836  infssd  29837  xrge0tsmsd  30132  ordtrest2NEW  30316  pwsiga  30540  measiun  30628  dya2iocuni  30692  bnj518  31300  bnj1137  31407  bnj1136  31409  bnj1413  31447  bnj1417  31453  bnj60  31474  erdszelem8  31524  cvmsss2  31600  cvmfolem  31605  dfon2lem8  32036  dfon2lem9  32037  dfon2  32038  rdgprc  32041  trpredtr  32071  trpredmintr  32072  trpredelss  32073  dftrpred3g  32074  trpredpo  32076  trpredrec  32079  frr3g  32121  frrlem5b  32127  frrlem5d  32129  sltval2  32151  nolesgn2ores  32167  nosupres  32195  nosupbnd2lem1  32203  scutun12  32259  nn0prpwlem  32659  ntruni  32664  clsint2  32666  fneint  32685  fnessref  32694  refssfne  32695  neibastop1  32696  neibastop2lem  32697  bj-0int  33384  bj-ismooredr2  33394  relowlpssretop  33546  heicant  33775  mblfinlem1  33777  ftc2nc  33824  sdclem2  33867  fdc  33870  seqpo  33872  prdsbnd  33921  heibor  33949  rrnequiv  33963  0idl  34153  intidl  34157  unichnidl  34159  prnc  34195  uniqsALTV  34434  lsmcv2  34827  lcvexchlem4  34835  lcvexchlem5  34836  eqlkr  34897  paddclN  35640  pclfinN  35698  ldilcnv  35913  ldilco  35914  cdleme25dN  36154  cdlemj2  36620  tendocan  36622  erng1lem  36785  erngdvlem4-rN  36797  dihord2pre  37023  dihglblem2N  37092  dochvalr  37155  hdmap14lem12  37677  hdmap14lem13  37678  pellfundre  37964  pellfundge  37965  pellfundlb  37967  dford3lem1  38111  aomclem2  38143  pwinfi3  38385  iunrelexp0  38511  iunrelexpmin1  38517  iunrelexpmin2  38521  dftrcl3  38529  cnvtrclfv  38533  trclimalb2  38535  dfrtrcl3  38542  ntrneiel2  38901  ntrneik4w  38915  ntrrn  38937  gneispa  38945  gneispb  38946  addrcom  39194  iunconnlem2  39682  ssuzfz  40062  dvmptfprod  40657  dvnprodlem3  40660  funressnfv  41679  tz6.12-afv  41779  tz6.12-afv2  41846  otiunsndisjX  41886  iccpartltu  41953  iccpartgtl  41954  iccpartleu  41956  iccpartgel  41957  fargshiftf  41968  fargshiftfva  41971  sbgoldbst  42258  bgoldbtbnd  42289  tgblthelfgott  42295  nnsgrp  42402  ellcoellss  42809  lindsrng01  42842  suppdm  42885  nn0sumshdiglem1  43000  setrec2fun  43024