Theorem ralrimiv 3139

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912

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

This theorem is referenced by:  ralrimiva  3140  ralrimivw  3144  ralrimdv  3146  reximdvaiOLD  3160  ralrimivv  3192  raleleq  3314  rr19.3v  3608  rabssdv  4019  rzalALT  4452  disjord  5075  disjiund  5077  trin  5216  class2seteq  5292  ralxfrALT  5353  otiunsndisj  5453  onmindif  6380  fnprb  7124  fntpb  7125  f1cdmsn  7194  ssorduni  7671  onminex  7694  onmindif2  7699  sucexeloniOLD  7702  suceloniOLD  7704  limuni3  7745  frxp  8013  poxp  8015  wfrlem15OLD  8203  onfununi  8221  onnseq  8224  tfrlem12  8269  tz7.48-2  8322  oaass  8442  omass  8461  oelim2  8476  oelimcl  8481  oaabs2  8529  omabs  8531  undifixp  8772  dom2lem  8832  isinf  9104  isinfOLD  9105  unblem4  9142  unbnn2  9144  marypha1lem  9269  supiso  9311  ordiso2  9351  card2inf  9391  elirrv  9432  wemapwe  9533  ttrclss  9556  trcl  9564  frr3g  9592  tz9.13  9627  rankval3b  9662  rankunb  9686  rankuni2b  9689  scott0  9722  updjud  9770  dfac8alem  9865  carduniima  9932  alephsmo  9938  alephval3  9946  iunfictbso  9950  dfac3  9957  dfac5lem5  9963  dfac12r  9982  dfac12k  9983  kmlem4  9989  kmlem11  9996  cfsuc  10093  cofsmo  10105  cfsmolem  10106  coftr  10109  alephsing  10112  infpssrlem3  10141  fin23lem30  10178  isf32lem2  10190  isf32lem3  10191  isf34lem6  10216  fin1a2lem11  10246  fin1a2lem13  10248  fin1a2s  10250  axcc2lem  10272  domtriomlem  10278  axdc3lem2  10287  axdc4lem  10291  axcclem  10293  axdclem2  10356  iundom2g  10376  uniimadom  10380  cardmin  10400  alephval2  10408  alephreg  10418  fpwwe2lem11  10477  wunex2  10574  wuncval2  10583  tskwe2  10609  inar1  10611  tskuni  10619  gruun  10642  intgru  10650  grutsk1  10657  genpcl  10844  ltexprlem5  10876  suplem1pr  10888  supexpr  10890  supsrlem  10947  axpre-sup  11005  negfi  12004  supaddc  12022  supadd  12023  supmul1  12024  supmullem1  12025  supmul  12027  peano5nni  12056  uzind  12492  zindd  12501  uzwo  12731  lbzbi  12756  xrsupsslem  13121  xrinfmsslem  13122  supxrun  13130  supxrpnf  13132  supxrunb1  13133  supxrunb2  13134  icoshftf1o  13286  flval3  13615  axdc4uzlem  13783  wrdnfi  14330  ccatrn  14373  ccatalpha  14377  2cshw  14605  cshweqrep  14613  s3iunsndisj  14758  rtrclreclem4  14851  dfrtrcl2  14852  sqrlem1  15033  sqrlem6  15038  fsum0diag2  15574  alzdvds  16108  gcdcllem1  16285  lcmfunsnlem2lem1  16420  lcmfunsnlem2lem2  16421  maxprmfct  16491  hashgcdeq  16567  unbenlem  16686  vdwlem6  16764  vdwlem10  16768  firest  17220  mrieqv2d  17425  iscatd  17459  initoeu2  17808  setcmon  17879  setcepi  17880  fullestrcsetc  17945  fullsetcestrc  17960  isglbd  18304  isacs4lem  18339  acsfiindd  18348  acsmapd  18349  psss  18375  sgrpidmnd  18467  pwmnd  18652  ghmrn  18923  ghmpreima  18932  cntz2ss  19015  symgextres  19109  psgnunilem2  19179  lsmsubg  19335  efgsfo  19420  gsumzaddlem  19597  gsummptnn0fzfv  19663  dmdprdd  19677  dprd2da  19720  ablsimpgprmd  19793  imasring  19933  isabvd  20163  issrngd  20204  islssd  20280  lbsextlem3  20505  lbsextlem4  20506  lidldvgen  20609  psgnghm  20868  isphld  20942  frlmsslsp  21086  mp2pm2mplem4  22041  tgcl  22202  distop  22228  indistopon  22234  pptbas  22241  toponmre  22327  opnnei  22354  neiuni  22356  neindisj2  22357  ordtrest2  22438  cnpnei  22498  cnindis  22526  cmpcld  22636  uncmp  22637  hauscmplem  22640  2ndc1stc  22685  1stcrest  22687  1stcelcls  22695  llyrest  22719  nllyrest  22720  cldllycmp  22729  reftr  22748  locfincf  22765  comppfsc  22766  txcls  22838  ptpjcn  22845  ptclsg  22849  dfac14lem  22851  xkoccn  22853  txlly  22870  txnlly  22871  ptrescn  22873  tx1stc  22884  xkoco1cn  22891  xkoco2cn  22892  xkococn  22894  xkoinjcn  22921  qtopeu  22950  hmeofval  22992  ordthmeolem  23035  isfild  23092  fbasrn  23118  trfil2  23121  flimclslem  23218  fclsrest  23258  fclscf  23259  flimfcls  23260  alexsubALTlem1  23281  alexsubALTlem2  23282  alexsubALTlem3  23283  alexsubALT  23285  qustgpopn  23354  isxmetd  23562  imasdsf1olem  23609  blcls  23745  prdsxmslem2  23768  metustfbas  23796  dscmet  23811  nrmmetd  23813  reperflem  24064  reconnlem2  24073  xrge0tsms  24080  fsumcn  24116  cnheibor  24201  tcphcph  24484  lmmbr  24505  caubl  24555  ivthlem1  24698  ovolctb  24737  ovoliunlem2  24750  ovolscalem1  24760  ovolicc2  24769  voliunlem3  24799  ismbfd  24886  mbfimaopnlem  24902  itg2le  24987  ellimc2  25124  c1liplem1  25243  plyeq0lem  25454  dgreq0  25509  aannenlem1  25571  pilem2  25694  cxpcn3lem  25983  scvxcvx  26218  musum  26423  dchrisum0flb  26741  ostth2lem2  26865  sltval2  26887  nolesgn2ores  26903  nogesgn1ores  26905  numedglnl  27650  upgrreslem  27807  umgrreslem  27808  nbuhgr  27846  nbumgr  27850  uhgrnbgr0nb  27857  nbusgrf1o0  27872  uvtxnbgrvtx  27896  cusgrfilem2  27959  uspgr2wlkeq  28149  wwlks  28336  iswwlksnon  28354  rusgr0edg  28474  clwwlkccatlem  28489  clwwisshclwwslem  28514  clwwlkn  28526  clwwlknon  28590  3cyclfrgrrn  28786  vdgn1frgrv3  28797  2wspmdisj  28837  numclwlk2lem2f1o  28879  frgrregord013  28895  htthlem  29415  ocsh  29781  shintcli  29827  pjss2coi  30662  pjnormssi  30666  pjclem4  30697  pj3si  30705  pj3cor1i  30707  strlem3a  30750  strb  30756  hstrlem3a  30758  hstrbi  30764  spansncv2  30791  mdsl1i  30819  cvmdi  30822  mdexchi  30833  h1da  30847  mdsymlem6  30906  sumdmdii  30913  dmdbr5ati  30920  isoun  31169  supssd  31179  infssd  31180  xrge0tsmsd  31452  ordtrest2NEW  32013  pwsiga  32238  measiun  32326  dya2iocuni  32390  bnj518  33005  bnj1137  33114  bnj1136  33116  bnj1413  33154  bnj1417  33160  bnj60  33181  subgrwlk  33233  erdszelem8  33299  cvmsss2  33375  cvmfolem  33380  fmlasucdisj  33500  satfun  33512  dfon2lem8  33897  dfon2lem9  33898  dfon2  33899  rdgprc  33901  sexp2  33923  sexp3  33929  nosupres  33984  nosupbnd2lem1  33992  noinfres  33999  noinfbnd2lem1  34007  scutun12  34078  madebdayim  34144  nn0prpwlem  34585  ntruni  34590  clsint2  34592  fneint  34611  fnessref  34620  refssfne  34621  neibastop1  34622  neibastop2lem  34623  bj-0int  35344  bj-ismooredr  35352  relowlpssretop  35607  fvineqsneu  35654  fvineqsneq  35655  heicant  35884  mblfinlem1  35886  ftc2nc  35931  sdclem2  35972  fdc  35975  seqpo  35977  prdsbnd  36023  heibor  36051  rrnequiv  36065  0idl  36255  intidl  36259  unichnidl  36261  prnc  36297  uniqsALTV  36562  refressn  36677  lsmcv2  37263  lcvexchlem4  37271  lcvexchlem5  37272  eqlkr  37333  paddclN  38077  pclfinN  38135  ldilcnv  38350  ldilco  38351  cdleme25dN  38591  cdlemj2  39057  tendocan  39059  erng1lem  39222  erngdvlem4-rN  39234  dihord2pre  39460  dihglblem2N  39529  dochvalr  39592  hdmap14lem12  40114  hdmap14lem13  40115  fsuppind  40495  pellfundre  40919  pellfundge  40920  pellfundlb  40922  dford3lem1  41065  aomclem2  41097  ofoafg  41266  naddcnff  41274  pwinfi3  41404  iunrelexp0  41544  iunrelexpmin1  41550  iunrelexpmin2  41554  dftrcl3  41562  cnvtrclfv  41566  trclimalb2  41568  dfrtrcl3  41575  ntrneiel2  41930  ntrneik4w  41944  ntrrn  41966  gneispa  41974  gneispb  41975  addrcom  42327  iunconnlem2  42789  ssuzfz  43137  dvmptfprod  43736  dvnprodlem3  43739  funressnfv  44802  cfsetsnfsetfo  44819  tz6.12-afv  44930  tz6.12-afv2  44997  otiunsndisjX  45036  uniimaprimaeqfv  45099  iccpartltu  45142  iccpartgtl  45143  iccpartleu  45145  iccpartgel  45146  fargshiftf  45157  fargshiftfva  45160  sbgoldbst  45495  bgoldbtbnd  45526  tgblthelfgott  45532  isomushgr  45543  nnsgrp  45636  ellcoellss  46041  lindsrng01  46074  suppdm  46116  nn0sumshdiglem1  46232  setrec2fun  46663