Theorem ralrimiv 3094

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

Syntax hints:   → wi 4   ∈ wcel 2112  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-ral 3056

This theorem is referenced by:  ralrimiva  3095  ralrimivw  3096  ralrimdv  3099  ralrimivv  3101  reximdvai  3181  raleleq  3323  rr19.3v  3566  rabssdv  3974  rzalALT  4407  disjord  5027  disjiund  5029  trin  5156  class2seteq  5231  ralxfrALT  5293  otiunsndisj  5388  onmindif  6280  fnprb  7002  fntpb  7003  ssorduni  7541  onminex  7564  onmindif2  7569  suceloni  7570  limuni3  7609  frxp  7871  poxp  7873  wfrlem15  8047  onfununi  8056  onnseq  8059  tfrlem12  8103  tz7.48-2  8156  oaass  8267  omass  8286  oelim2  8301  oelimcl  8306  oaabs2  8352  omabs  8354  undifixp  8593  dom2lem  8646  isinf  8867  unblem4  8904  unbnn2  8906  marypha1lem  9027  supiso  9069  ordiso2  9109  card2inf  9149  elirrv  9190  wemapwe  9290  trpredtr  9313  trpredmintr  9314  trpredelss  9316  dftrpred3g  9317  trpredpo  9319  trpredrec  9320  trcl  9322  tz9.13  9372  rankval3b  9407  rankunb  9431  rankuni2b  9434  scott0  9467  updjud  9515  dfac8alem  9608  carduniima  9675  alephsmo  9681  alephval3  9689  iunfictbso  9693  dfac3  9700  dfac5lem5  9706  dfac12r  9725  dfac12k  9726  kmlem4  9732  kmlem11  9739  cfsuc  9836  cofsmo  9848  cfsmolem  9849  coftr  9852  alephsing  9855  infpssrlem3  9884  fin23lem30  9921  isf32lem2  9933  isf32lem3  9934  isf34lem6  9959  fin1a2lem11  9989  fin1a2lem13  9991  fin1a2s  9993  axcc2lem  10015  domtriomlem  10021  axdc3lem2  10030  axdc4lem  10034  axcclem  10036  axdclem2  10099  iundom2g  10119  uniimadom  10123  cardmin  10143  alephval2  10151  alephreg  10161  fpwwe2lem11  10220  wunex2  10317  wuncval2  10326  tskwe2  10352  inar1  10354  tskuni  10362  gruun  10385  intgru  10393  grutsk1  10400  genpcl  10587  ltexprlem5  10619  suplem1pr  10631  supexpr  10633  supsrlem  10690  axpre-sup  10748  negfi  11746  supaddc  11764  supadd  11765  supmul1  11766  supmullem1  11767  supmul  11769  peano5nni  11798  uzind  12234  zindd  12243  uzwo  12472  lbzbi  12497  xrsupsslem  12862  xrinfmsslem  12863  supxrun  12871  supxrpnf  12873  supxrunb1  12874  supxrunb2  12875  icoshftf1o  13027  flval3  13355  axdc4uzlem  13521  wrdnfi  14068  ccatrn  14111  ccatalpha  14115  2cshw  14343  cshweqrep  14351  s3iunsndisj  14496  rtrclreclem4  14589  dfrtrcl2  14590  sqrlem1  14771  sqrlem6  14776  fsum0diag2  15310  alzdvds  15844  gcdcllem1  16021  lcmfunsnlem2lem1  16158  lcmfunsnlem2lem2  16159  maxprmfct  16229  hashgcdeq  16305  unbenlem  16424  vdwlem6  16502  vdwlem10  16506  firest  16891  mrieqv2d  17096  iscatd  17130  initoeu2  17476  setcmon  17547  setcepi  17548  fullestrcsetc  17612  fullsetcestrc  17627  isglbd  17969  isacs4lem  18004  acsfiindd  18013  acsmapd  18014  psss  18040  sgrpidmnd  18132  pwmnd  18318  ghmrn  18589  ghmpreima  18598  cntz2ss  18681  symgextres  18771  psgnunilem2  18841  lsmsubg  18997  efgsfo  19083  gsumzaddlem  19260  gsummptnn0fzfv  19326  dmdprdd  19340  dprd2da  19383  ablsimpgprmd  19456  imasring  19591  isabvd  19810  issrngd  19851  islssd  19926  lbsextlem3  20151  lbsextlem4  20152  lidldvgen  20247  psgnghm  20496  isphld  20570  frlmsslsp  20712  mp2pm2mplem4  21660  tgcl  21820  distop  21846  indistopon  21852  pptbas  21859  toponmre  21944  opnnei  21971  neiuni  21973  neindisj2  21974  ordtrest2  22055  cnpnei  22115  cnindis  22143  cmpcld  22253  uncmp  22254  hauscmplem  22257  2ndc1stc  22302  1stcrest  22304  1stcelcls  22312  llyrest  22336  nllyrest  22337  cldllycmp  22346  reftr  22365  locfincf  22382  comppfsc  22383  txcls  22455  ptpjcn  22462  ptclsg  22466  dfac14lem  22468  xkoccn  22470  txlly  22487  txnlly  22488  ptrescn  22490  tx1stc  22501  xkoco1cn  22508  xkoco2cn  22509  xkococn  22511  xkoinjcn  22538  qtopeu  22567  hmeofval  22609  ordthmeolem  22652  isfild  22709  fbasrn  22735  trfil2  22738  flimclslem  22835  fclsrest  22875  fclscf  22876  flimfcls  22877  alexsubALTlem1  22898  alexsubALTlem2  22899  alexsubALTlem3  22900  alexsubALT  22902  qustgpopn  22971  isxmetd  23178  imasdsf1olem  23225  blcls  23358  prdsxmslem2  23381  metustfbas  23409  dscmet  23424  nrmmetd  23426  reperflem  23669  reconnlem2  23678  xrge0tsms  23685  fsumcn  23721  cnheibor  23806  tcphcph  24088  lmmbr  24109  caubl  24159  ivthlem1  24302  ovolctb  24341  ovoliunlem2  24354  ovolscalem1  24364  ovolicc2  24373  voliunlem3  24403  ismbfd  24490  mbfimaopnlem  24506  itg2le  24591  ellimc2  24728  c1liplem1  24847  plyeq0lem  25058  dgreq0  25113  aannenlem1  25175  pilem2  25298  cxpcn3lem  25587  scvxcvx  25822  musum  26027  dchrisum0flb  26345  ostth2lem2  26469  numedglnl  27189  upgrreslem  27346  umgrreslem  27347  nbuhgr  27385  nbumgr  27389  uhgrnbgr0nb  27396  nbusgrf1o0  27411  uvtxnbgrvtx  27435  cusgrfilem2  27498  uspgr2wlkeq  27687  wwlks  27873  iswwlksnon  27891  rusgr0edg  28011  clwwlkccatlem  28026  clwwisshclwwslem  28051  clwwlkn  28063  clwwlknon  28127  3cyclfrgrrn  28323  vdgn1frgrv3  28334  2wspmdisj  28374  numclwlk2lem2f1o  28416  frgrregord013  28432  htthlem  28952  ocsh  29318  shintcli  29364  pjss2coi  30199  pjnormssi  30203  pjclem4  30234  pj3si  30242  pj3cor1i  30244  strlem3a  30287  strb  30293  hstrlem3a  30295  hstrbi  30301  spansncv2  30328  mdsl1i  30356  cvmdi  30359  mdexchi  30370  h1da  30384  mdsymlem6  30443  sumdmdii  30450  dmdbr5ati  30457  isoun  30708  supssd  30718  infssd  30719  xrge0tsmsd  30990  ordtrest2NEW  31541  pwsiga  31764  measiun  31852  dya2iocuni  31916  bnj518  32533  bnj1137  32642  bnj1136  32644  bnj1413  32682  bnj1417  32688  bnj60  32709  subgrwlk  32761  erdszelem8  32827  cvmsss2  32903  cvmfolem  32908  fmlasucdisj  33028  satfun  33040  dfon2lem8  33436  dfon2lem9  33437  dfon2  33438  rdgprc  33440  sexp2  33473  sexp3  33479  frr3g  33504  sltval2  33545  nolesgn2ores  33561  nogesgn1ores  33563  nosupres  33596  nosupbnd2lem1  33604  noinfres  33611  noinfbnd2lem1  33619  scutun12  33690  madebdayim  33756  nn0prpwlem  34197  ntruni  34202  clsint2  34204  fneint  34223  fnessref  34232  refssfne  34233  neibastop1  34234  neibastop2lem  34235  bj-0int  34956  bj-ismooredr  34964  relowlpssretop  35221  fvineqsneu  35268  fvineqsneq  35269  heicant  35498  mblfinlem1  35500  ftc2nc  35545  sdclem2  35586  fdc  35589  seqpo  35591  prdsbnd  35637  heibor  35665  rrnequiv  35679  0idl  35869  intidl  35873  unichnidl  35875  prnc  35911  uniqsALTV  36150  lsmcv2  36729  lcvexchlem4  36737  lcvexchlem5  36738  eqlkr  36799  paddclN  37542  pclfinN  37600  ldilcnv  37815  ldilco  37816  cdleme25dN  38056  cdlemj2  38522  tendocan  38524  erng1lem  38687  erngdvlem4-rN  38699  dihord2pre  38925  dihglblem2N  38994  dochvalr  39057  hdmap14lem12  39579  hdmap14lem13  39580  fsuppind  39930  pellfundre  40347  pellfundge  40348  pellfundlb  40350  dford3lem1  40492  aomclem2  40524  pwinfi3  40787  iunrelexp0  40928  iunrelexpmin1  40934  iunrelexpmin2  40938  dftrcl3  40946  cnvtrclfv  40950  trclimalb2  40952  dfrtrcl3  40959  ntrneiel2  41314  ntrneik4w  41328  ntrrn  41350  gneispa  41358  gneispb  41359  addrcom  41707  iunconnlem2  42169  ssuzfz  42502  dvmptfprod  43104  dvnprodlem3  43107  funressnfv  44152  cfsetsnfsetfo  44169  tz6.12-afv  44280  tz6.12-afv2  44347  otiunsndisjX  44386  uniimaprimaeqfv  44450  iccpartltu  44493  iccpartgtl  44494  iccpartleu  44496  iccpartgel  44497  fargshiftf  44508  fargshiftfva  44511  sbgoldbst  44846  bgoldbtbnd  44877  tgblthelfgott  44883  isomushgr  44894  nnsgrp  44987  ellcoellss  45392  lindsrng01  45425  suppdm  45467  nn0sumshdiglem1  45583  setrec2fun  46012