Theorem ralrimiv 3128

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 3127	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

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

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 1912

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

This theorem is referenced by:  ralrimiva  3129  ralrimivw  3133  ralrimdv  3135  ralrimivv  3178  rr19.3v  3622  class2seteq  3663  rabssdv  4027  rzalALT  4449  r19.3rzv  4457  disjord  5088  disjiund  5090  trin  5217  ralxfrALT  5361  otiunsndisj  5469  onmindif  6412  fnprb  7156  fntpb  7157  f1cdmsn  7230  ssorduni  7726  onminex  7749  onmindif2  7754  limuni3  7796  frxp  8070  poxp  8072  sexp2  8090  sexp3  8097  onfununi  8275  onnseq  8278  tfrlem12  8322  tz7.48-2  8375  oaass  8490  omass  8509  oelim2  8525  oelimcl  8530  oaabs2  8579  omabs  8581  uniqs  8714  undifixp  8876  dom2lem  8933  isinf  9169  unblem4  9199  unbnn2  9201  marypha1lem  9340  supssd  9370  supiso  9383  infssd  9401  ordiso2  9424  card2inf  9464  elirrvOLD  9507  wemapwe  9610  ttrclss  9633  trcl  9641  frr3g  9672  tz9.13  9707  rankval3b  9742  rankunb  9766  rankuni2b  9769  scott0  9802  updjud  9850  dfac8alem  9943  carduniima  10010  alephsmo  10016  alephval3  10024  iunfictbso  10028  dfac3  10035  dfac5lem5  10041  dfac12r  10061  dfac12k  10062  kmlem4  10068  kmlem11  10075  cfsuc  10171  cofsmo  10183  cfsmolem  10184  coftr  10187  alephsing  10190  infpssrlem3  10219  fin23lem30  10256  isf32lem2  10268  isf32lem3  10269  isf34lem6  10294  fin1a2lem11  10324  fin1a2lem13  10326  fin1a2s  10328  axcc2lem  10350  domtriomlem  10356  axdc3lem2  10365  axdc4lem  10369  axcclem  10371  axdclem2  10434  iundom2g  10454  uniimadom  10458  cardmin  10478  alephval2  10487  alephreg  10497  fpwwe2lem11  10556  wunex2  10653  wuncval2  10662  tskwe2  10688  inar1  10690  tskuni  10698  gruun  10721  intgru  10729  grutsk1  10736  genpcl  10923  ltexprlem5  10955  suplem1pr  10967  supexpr  10969  supsrlem  11026  axpre-sup  11084  negfi  12095  supaddc  12113  supadd  12114  supmul1  12115  supmullem1  12116  supmul  12118  peano5nni  12152  uzind  12588  zindd  12597  uzwo  12828  lbzbi  12853  xrsupsslem  13226  xrinfmsslem  13227  supxrun  13235  supxrpnf  13237  supxrunb1  13238  supxrunb2  13239  icoshftf1o  13394  flval3  13739  axdc4uzlem  13910  tpfo  14427  wrdnfi  14475  ccatrn  14517  ccatalpha  14521  2cshw  14740  cshweqrep  14748  s3iunsndisj  14895  rtrclreclem4  14988  dfrtrcl2  14989  01sqrexlem1  15169  01sqrexlem6  15174  fsum0diag2  15710  alzdvds  16251  gcdcllem1  16430  lcmfunsnlem2lem1  16569  lcmfunsnlem2lem2  16570  maxprmfct  16640  hashgcdeq  16721  unbenlem  16840  vdwlem6  16918  vdwlem10  16922  firest  17356  mrieqv2d  17566  iscatd  17600  initoeu2  17944  setcmon  18015  setcepi  18016  fullestrcsetc  18078  fullsetcestrc  18093  isglbd  18436  isacs4lem  18471  acsfiindd  18480  acsmapd  18481  psss  18507  sgrpidmnd  18668  pwmnd  18866  ghmrn  19162  ghmpreima  19171  cntz2ss  19268  symgextres  19358  psgnunilem2  19428  lsmsubg  19587  efgsfo  19672  gsumzaddlem  19854  gsummptnn0fzfv  19920  dmdprdd  19934  dprd2da  19977  ablsimpgprmd  20050  imasring  20270  01eq0ring  20467  isabvd  20749  issrngd  20792  islssd  20890  lbsextlem3  21119  lbsextlem4  21120  lidldvgen  21293  pzriprnglem4  21443  pzriprnglem7  21446  pzriprnglem13  21452  psgnghm  21539  isphld  21613  frlmsslsp  21755  mp2pm2mplem4  22757  tgcl  22917  distop  22943  indistopon  22949  pptbas  22956  toponmre  23041  opnnei  23068  neiuni  23070  neindisj2  23071  ordtrest2  23152  cnpnei  23212  cnindis  23240  cmpcld  23350  uncmp  23351  hauscmplem  23354  2ndc1stc  23399  1stcrest  23401  1stcelcls  23409  llyrest  23433  nllyrest  23434  cldllycmp  23443  reftr  23462  locfincf  23479  comppfsc  23480  txcls  23552  ptpjcn  23559  ptclsg  23563  dfac14lem  23565  xkoccn  23567  txlly  23584  txnlly  23585  ptrescn  23587  tx1stc  23598  xkoco1cn  23605  xkoco2cn  23606  xkococn  23608  xkoinjcn  23635  qtopeu  23664  hmeofval  23706  ordthmeolem  23749  isfild  23806  fbasrn  23832  trfil2  23835  flimclslem  23932  fclsrest  23972  fclscf  23973  flimfcls  23974  alexsubALTlem1  23995  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALT  23999  qustgpopn  24068  isxmetd  24274  imasdsf1olem  24321  blcls  24454  prdsxmslem2  24477  metustfbas  24505  dscmet  24520  nrmmetd  24522  reperflem  24767  reconnlem2  24776  xrge0tsms  24783  fsumcn  24821  cnheibor  24914  tcphcph  25197  lmmbr  25218  caubl  25268  ivthlem1  25412  ovolctb  25451  ovoliunlem2  25464  ovolscalem1  25474  ovolicc2  25483  voliunlem3  25513  ismbfd  25600  mbfimaopnlem  25616  itg2le  25700  ellimc2  25838  c1liplem1  25961  plyeq0lem  26175  dgreq0  26231  aannenlem1  26296  pilem2  26422  cxpcn3lem  26717  scvxcvx  26956  musum  27161  fsumdvdsmul  27165  dchrisum0flb  27481  ostth2lem2  27605  ltsval2  27628  nolesgn2ores  27644  nogesgn1ores  27646  nosupres  27679  nosupbnd2lem1  27687  noinfres  27694  noinfbnd2lem1  27702  cutsun12  27790  madebdayim  27888  precsexlem9  28215  addonbday  28279  noseqind  28292  z12zsodd  28482  numedglnl  29221  upgrreslem  29381  umgrreslem  29382  nbuhgr  29420  nbumgr  29424  uhgrnbgr0nb  29431  nbusgrf1o0  29446  uvtxnbgrvtx  29470  cusgrfilem2  29534  uspgr2wlkeq  29723  wwlks  29912  iswwlksnon  29930  rusgr0edg  30053  clwwlkccatlem  30068  clwwisshclwwslem  30093  clwwlkn  30105  clwwlknon  30169  3cyclfrgrrn  30365  vdgn1frgrv3  30376  2wspmdisj  30416  numclwlk2lem2f1o  30458  frgrregord013  30474  htthlem  30996  ocsh  31362  shintcli  31408  pjss2coi  32243  pjnormssi  32247  pjclem4  32278  pj3si  32286  pj3cor1i  32288  strlem3a  32331  strb  32337  hstrlem3a  32339  hstrbi  32345  spansncv2  32372  mdsl1i  32400  cvmdi  32403  mdexchi  32414  h1da  32428  mdsymlem6  32487  sumdmdii  32494  dmdbr5ati  32501  isoun  32783  xrge0tsmsd  33157  ordtrest2NEW  34082  pwsiga  34289  measiun  34377  dya2iocuni  34442  bnj518  35044  bnj1137  35153  bnj1136  35155  bnj1413  35193  bnj1417  35199  bnj60  35220  rankval4b  35258  r1filim  35262  trssfir1om  35269  fineqvnttrclselem3  35281  fineqvinfep  35283  tz9.1regs  35292  trssfir1omregs  35294  gblacfnacd  35298  onvf1odlem1  35299  onvf1odlem4  35302  subgrwlk  35328  erdszelem8  35394  cvmsss2  35470  cvmfolem  35475  fmlasucdisj  35595  satfun  35607  dfon2lem8  35984  dfon2lem9  35985  dfon2  35986  rdgprc  35988  nn0prpwlem  36518  ntruni  36523  clsint2  36525  fneint  36544  fnessref  36553  refssfne  36554  neibastop1  36555  neibastop2lem  36556  bj-0int  37308  bj-ismooredr  37316  relowlpssretop  37571  fvineqsneu  37618  fvineqsneq  37619  heicant  37858  mblfinlem1  37860  ftc2nc  37905  sdclem2  37945  fdc  37948  seqpo  37950  prdsbnd  37996  heibor  38024  rrnequiv  38038  0idl  38228  intidl  38232  unichnidl  38234  prnc  38270  refressn  38736  lsmcv2  39357  lcvexchlem4  39365  lcvexchlem5  39366  eqlkr  39427  paddclN  40170  pclfinN  40228  ldilcnv  40443  ldilco  40444  cdleme25dN  40684  cdlemj2  41150  tendocan  41152  erng1lem  41315  erngdvlem4-rN  41327  dihord2pre  41553  dihglblem2N  41622  dochvalr  41685  hdmap14lem12  42207  hdmap14lem13  42208  supinf  42564  fsuppind  42900  pellfundre  43190  pellfundge  43191  pellfundlb  43193  dford3lem1  43335  aomclem2  43364  oaabsb  43603  cantnf2  43634  ofoafg  43663  naddcnff  43671  naddwordnexlem3  43708  naddwordnexlem4  43710  pwinfi3  43871  iunrelexp0  44010  iunrelexpmin1  44016  iunrelexpmin2  44020  dftrcl3  44028  cnvtrclfv  44032  trclimalb2  44034  dfrtrcl3  44041  ntrneiel2  44394  ntrneik4w  44408  ntrrn  44430  gneispa  44438  gneispb  44439  addrcom  44782  iunconnlem2  45242  ssuzfz  45661  dvnprodlem3  46259  funressnfv  47356  cfsetsnfsetfo  47373  tz6.12-afv  47486  tz6.12-afv2  47553  otiunsndisjX  47592  uniimaprimaeqfv  47695  iccpartltu  47738  iccpartgtl  47739  iccpartleu  47741  iccpartgel  47742  fargshiftf  47753  fargshiftfva  47756  sbgoldbst  48091  bgoldbtbnd  48122  tgblthelfgott  48128  grimuhgr  48200  grimco  48202  isuspgrim0  48207  isuspgrimlem  48208  upgrimpths  48222  gricushgr  48230  grtriclwlk3  48258  stgr0  48273  uspgrlim  48305  grlicsym  48326  nnsgrp  48490  ellcoellss  48748  lindsrng01  48781  suppdm  48823  nn0sumshdiglem1  48934  setrec2fun  50004