Theorem ralrimiv 3106

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

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

This theorem is referenced by:  ralrimiva  3107  ralrimivw  3108  ralrimdv  3111  ralrimivv  3113  reximdvaiOLD  3200  raleleq  3347  rr19.3v  3591  rabssdv  4004  rzalALT  4437  disjord  5058  disjiund  5060  trin  5197  class2seteq  5272  ralxfrALT  5333  otiunsndisj  5428  onmindif  6340  fnprb  7066  fntpb  7067  ssorduni  7606  onminex  7629  onmindif2  7634  suceloni  7635  limuni3  7674  frxp  7938  poxp  7940  wfrlem15OLD  8125  onfununi  8143  onnseq  8146  tfrlem12  8191  tz7.48-2  8243  oaass  8354  omass  8373  oelim2  8388  oelimcl  8393  oaabs2  8439  omabs  8441  undifixp  8680  dom2lem  8735  isinf  8965  unblem4  8999  unbnn2  9001  marypha1lem  9122  supiso  9164  ordiso2  9204  card2inf  9244  elirrv  9285  wemapwe  9385  trpredtr  9408  trpredmintr  9409  trpredelss  9411  dftrpred3g  9412  trpredpo  9414  trpredrec  9415  trcl  9417  frr3g  9445  tz9.13  9480  rankval3b  9515  rankunb  9539  rankuni2b  9542  scott0  9575  updjud  9623  dfac8alem  9716  carduniima  9783  alephsmo  9789  alephval3  9797  iunfictbso  9801  dfac3  9808  dfac5lem5  9814  dfac12r  9833  dfac12k  9834  kmlem4  9840  kmlem11  9847  cfsuc  9944  cofsmo  9956  cfsmolem  9957  coftr  9960  alephsing  9963  infpssrlem3  9992  fin23lem30  10029  isf32lem2  10041  isf32lem3  10042  isf34lem6  10067  fin1a2lem11  10097  fin1a2lem13  10099  fin1a2s  10101  axcc2lem  10123  domtriomlem  10129  axdc3lem2  10138  axdc4lem  10142  axcclem  10144  axdclem2  10207  iundom2g  10227  uniimadom  10231  cardmin  10251  alephval2  10259  alephreg  10269  fpwwe2lem11  10328  wunex2  10425  wuncval2  10434  tskwe2  10460  inar1  10462  tskuni  10470  gruun  10493  intgru  10501  grutsk1  10508  genpcl  10695  ltexprlem5  10727  suplem1pr  10739  supexpr  10741  supsrlem  10798  axpre-sup  10856  negfi  11854  supaddc  11872  supadd  11873  supmul1  11874  supmullem1  11875  supmul  11877  peano5nni  11906  uzind  12342  zindd  12351  uzwo  12580  lbzbi  12605  xrsupsslem  12970  xrinfmsslem  12971  supxrun  12979  supxrpnf  12981  supxrunb1  12982  supxrunb2  12983  icoshftf1o  13135  flval3  13463  axdc4uzlem  13631  wrdnfi  14179  ccatrn  14222  ccatalpha  14226  2cshw  14454  cshweqrep  14462  s3iunsndisj  14607  rtrclreclem4  14700  dfrtrcl2  14701  sqrlem1  14882  sqrlem6  14887  fsum0diag2  15423  alzdvds  15957  gcdcllem1  16134  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  maxprmfct  16342  hashgcdeq  16418  unbenlem  16537  vdwlem6  16615  vdwlem10  16619  firest  17060  mrieqv2d  17265  iscatd  17299  initoeu2  17647  setcmon  17718  setcepi  17719  fullestrcsetc  17784  fullsetcestrc  17799  isglbd  18142  isacs4lem  18177  acsfiindd  18186  acsmapd  18187  psss  18213  sgrpidmnd  18305  pwmnd  18491  ghmrn  18762  ghmpreima  18771  cntz2ss  18854  symgextres  18948  psgnunilem2  19018  lsmsubg  19174  efgsfo  19260  gsumzaddlem  19437  gsummptnn0fzfv  19503  dmdprdd  19517  dprd2da  19560  ablsimpgprmd  19633  imasring  19773  isabvd  19995  issrngd  20036  islssd  20112  lbsextlem3  20337  lbsextlem4  20338  lidldvgen  20439  psgnghm  20697  isphld  20771  frlmsslsp  20913  mp2pm2mplem4  21866  tgcl  22027  distop  22053  indistopon  22059  pptbas  22066  toponmre  22152  opnnei  22179  neiuni  22181  neindisj2  22182  ordtrest2  22263  cnpnei  22323  cnindis  22351  cmpcld  22461  uncmp  22462  hauscmplem  22465  2ndc1stc  22510  1stcrest  22512  1stcelcls  22520  llyrest  22544  nllyrest  22545  cldllycmp  22554  reftr  22573  locfincf  22590  comppfsc  22591  txcls  22663  ptpjcn  22670  ptclsg  22674  dfac14lem  22676  xkoccn  22678  txlly  22695  txnlly  22696  ptrescn  22698  tx1stc  22709  xkoco1cn  22716  xkoco2cn  22717  xkococn  22719  xkoinjcn  22746  qtopeu  22775  hmeofval  22817  ordthmeolem  22860  isfild  22917  fbasrn  22943  trfil2  22946  flimclslem  23043  fclsrest  23083  fclscf  23084  flimfcls  23085  alexsubALTlem1  23106  alexsubALTlem2  23107  alexsubALTlem3  23108  alexsubALT  23110  qustgpopn  23179  isxmetd  23387  imasdsf1olem  23434  blcls  23568  prdsxmslem2  23591  metustfbas  23619  dscmet  23634  nrmmetd  23636  reperflem  23887  reconnlem2  23896  xrge0tsms  23903  fsumcn  23939  cnheibor  24024  tcphcph  24306  lmmbr  24327  caubl  24377  ivthlem1  24520  ovolctb  24559  ovoliunlem2  24572  ovolscalem1  24582  ovolicc2  24591  voliunlem3  24621  ismbfd  24708  mbfimaopnlem  24724  itg2le  24809  ellimc2  24946  c1liplem1  25065  plyeq0lem  25276  dgreq0  25331  aannenlem1  25393  pilem2  25516  cxpcn3lem  25805  scvxcvx  26040  musum  26245  dchrisum0flb  26563  ostth2lem2  26687  numedglnl  27417  upgrreslem  27574  umgrreslem  27575  nbuhgr  27613  nbumgr  27617  uhgrnbgr0nb  27624  nbusgrf1o0  27639  uvtxnbgrvtx  27663  cusgrfilem2  27726  uspgr2wlkeq  27915  wwlks  28101  iswwlksnon  28119  rusgr0edg  28239  clwwlkccatlem  28254  clwwisshclwwslem  28279  clwwlkn  28291  clwwlknon  28355  3cyclfrgrrn  28551  vdgn1frgrv3  28562  2wspmdisj  28602  numclwlk2lem2f1o  28644  frgrregord013  28660  htthlem  29180  ocsh  29546  shintcli  29592  pjss2coi  30427  pjnormssi  30431  pjclem4  30462  pj3si  30470  pj3cor1i  30472  strlem3a  30515  strb  30521  hstrlem3a  30523  hstrbi  30529  spansncv2  30556  mdsl1i  30584  cvmdi  30587  mdexchi  30598  h1da  30612  mdsymlem6  30671  sumdmdii  30678  dmdbr5ati  30685  isoun  30936  supssd  30946  infssd  30947  xrge0tsmsd  31219  ordtrest2NEW  31775  pwsiga  31998  measiun  32086  dya2iocuni  32150  bnj518  32766  bnj1137  32875  bnj1136  32877  bnj1413  32915  bnj1417  32921  bnj60  32942  subgrwlk  32994  erdszelem8  33060  cvmsss2  33136  cvmfolem  33141  fmlasucdisj  33261  satfun  33273  dfon2lem8  33672  dfon2lem9  33673  dfon2  33674  rdgprc  33676  ttrclss  33706  sexp2  33720  sexp3  33726  sltval2  33786  nolesgn2ores  33802  nogesgn1ores  33804  nosupres  33837  nosupbnd2lem1  33845  noinfres  33852  noinfbnd2lem1  33860  scutun12  33931  madebdayim  33997  nn0prpwlem  34438  ntruni  34443  clsint2  34445  fneint  34464  fnessref  34473  refssfne  34474  neibastop1  34475  neibastop2lem  34476  bj-0int  35199  bj-ismooredr  35207  relowlpssretop  35462  fvineqsneu  35509  fvineqsneq  35510  heicant  35739  mblfinlem1  35741  ftc2nc  35786  sdclem2  35827  fdc  35830  seqpo  35832  prdsbnd  35878  heibor  35906  rrnequiv  35920  0idl  36110  intidl  36114  unichnidl  36116  prnc  36152  uniqsALTV  36391  lsmcv2  36970  lcvexchlem4  36978  lcvexchlem5  36979  eqlkr  37040  paddclN  37783  pclfinN  37841  ldilcnv  38056  ldilco  38057  cdleme25dN  38297  cdlemj2  38763  tendocan  38765  erng1lem  38928  erngdvlem4-rN  38940  dihord2pre  39166  dihglblem2N  39235  dochvalr  39298  hdmap14lem12  39820  hdmap14lem13  39821  fsuppind  40202  pellfundre  40619  pellfundge  40620  pellfundlb  40622  dford3lem1  40764  aomclem2  40796  pwinfi3  41059  iunrelexp0  41199  iunrelexpmin1  41205  iunrelexpmin2  41209  dftrcl3  41217  cnvtrclfv  41221  trclimalb2  41223  dfrtrcl3  41230  ntrneiel2  41585  ntrneik4w  41599  ntrrn  41621  gneispa  41629  gneispb  41630  addrcom  41982  iunconnlem2  42444  ssuzfz  42778  dvmptfprod  43376  dvnprodlem3  43379  funressnfv  44424  cfsetsnfsetfo  44441  tz6.12-afv  44552  tz6.12-afv2  44619  otiunsndisjX  44658  uniimaprimaeqfv  44722  iccpartltu  44765  iccpartgtl  44766  iccpartleu  44768  iccpartgel  44769  fargshiftf  44780  fargshiftfva  44783  sbgoldbst  45118  bgoldbtbnd  45149  tgblthelfgott  45155  isomushgr  45166  nnsgrp  45259  ellcoellss  45664  lindsrng01  45697  suppdm  45739  nn0sumshdiglem1  45855  setrec2fun  46284