Theorem ralrimiv 3124

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  ralrimiva  3125  ralrimivw  3129  ralrimdv  3131  ralrimivv  3178  rr19.3v  3633  class2seteq  3675  rabssdv  4038  rzalALT  4473  disjord  5096  disjiund  5098  trin  5226  ralxfrALT  5370  otiunsndisj  5480  onmindif  6426  fnprb  7182  fntpb  7183  f1cdmsn  7257  ssorduni  7755  onminex  7778  onmindif2  7783  sucexeloniOLD  7786  limuni3  7828  frxp  8105  poxp  8107  sexp2  8125  sexp3  8132  onfununi  8310  onnseq  8313  tfrlem12  8357  tz7.48-2  8410  oaass  8525  omass  8544  oelim2  8559  oelimcl  8564  oaabs2  8613  omabs  8615  uniqs  8747  undifixp  8907  dom2lem  8963  isinf  9207  isinfOLD  9208  unblem4  9242  unbnn2  9244  marypha1lem  9384  supssd  9414  supiso  9427  infssd  9445  ordiso2  9468  card2inf  9508  elirrv  9549  wemapwe  9650  ttrclss  9673  trcl  9681  frr3g  9709  tz9.13  9744  rankval3b  9779  rankunb  9803  rankuni2b  9806  scott0  9839  updjud  9887  dfac8alem  9982  carduniima  10049  alephsmo  10055  alephval3  10063  iunfictbso  10067  dfac3  10074  dfac5lem5  10080  dfac12r  10100  dfac12k  10101  kmlem4  10107  kmlem11  10114  cfsuc  10210  cofsmo  10222  cfsmolem  10223  coftr  10226  alephsing  10229  infpssrlem3  10258  fin23lem30  10295  isf32lem2  10307  isf32lem3  10308  isf34lem6  10333  fin1a2lem11  10363  fin1a2lem13  10365  fin1a2s  10367  axcc2lem  10389  domtriomlem  10395  axdc3lem2  10404  axdc4lem  10408  axcclem  10410  axdclem2  10473  iundom2g  10493  uniimadom  10497  cardmin  10517  alephval2  10525  alephreg  10535  fpwwe2lem11  10594  wunex2  10691  wuncval2  10700  tskwe2  10726  inar1  10728  tskuni  10736  gruun  10759  intgru  10767  grutsk1  10774  genpcl  10961  ltexprlem5  10993  suplem1pr  11005  supexpr  11007  supsrlem  11064  axpre-sup  11122  negfi  12132  supaddc  12150  supadd  12151  supmul1  12152  supmullem1  12153  supmul  12155  peano5nni  12189  uzind  12626  zindd  12635  uzwo  12870  lbzbi  12895  xrsupsslem  13267  xrinfmsslem  13268  supxrun  13276  supxrpnf  13278  supxrunb1  13279  supxrunb2  13280  icoshftf1o  13435  flval3  13777  axdc4uzlem  13948  tpfo  14465  wrdnfi  14513  ccatrn  14554  ccatalpha  14558  2cshw  14778  cshweqrep  14786  s3iunsndisj  14934  rtrclreclem4  15027  dfrtrcl2  15028  01sqrexlem1  15208  01sqrexlem6  15213  fsum0diag2  15749  alzdvds  16290  gcdcllem1  16469  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  maxprmfct  16679  hashgcdeq  16760  unbenlem  16879  vdwlem6  16957  vdwlem10  16961  firest  17395  mrieqv2d  17600  iscatd  17634  initoeu2  17978  setcmon  18049  setcepi  18050  fullestrcsetc  18112  fullsetcestrc  18127  isglbd  18468  isacs4lem  18503  acsfiindd  18512  acsmapd  18513  psss  18539  sgrpidmnd  18666  pwmnd  18864  ghmrn  19161  ghmpreima  19170  cntz2ss  19267  symgextres  19355  psgnunilem2  19425  lsmsubg  19584  efgsfo  19669  gsumzaddlem  19851  gsummptnn0fzfv  19917  dmdprdd  19931  dprd2da  19974  ablsimpgprmd  20047  imasring  20239  01eq0ring  20439  isabvd  20721  issrngd  20764  islssd  20841  lbsextlem3  21070  lbsextlem4  21071  lidldvgen  21244  pzriprnglem4  21394  pzriprnglem7  21397  pzriprnglem13  21403  psgnghm  21489  isphld  21563  frlmsslsp  21705  mp2pm2mplem4  22696  tgcl  22856  distop  22882  indistopon  22888  pptbas  22895  toponmre  22980  opnnei  23007  neiuni  23009  neindisj2  23010  ordtrest2  23091  cnpnei  23151  cnindis  23179  cmpcld  23289  uncmp  23290  hauscmplem  23293  2ndc1stc  23338  1stcrest  23340  1stcelcls  23348  llyrest  23372  nllyrest  23373  cldllycmp  23382  reftr  23401  locfincf  23418  comppfsc  23419  txcls  23491  ptpjcn  23498  ptclsg  23502  dfac14lem  23504  xkoccn  23506  txlly  23523  txnlly  23524  ptrescn  23526  tx1stc  23537  xkoco1cn  23544  xkoco2cn  23545  xkococn  23547  xkoinjcn  23574  qtopeu  23603  hmeofval  23645  ordthmeolem  23688  isfild  23745  fbasrn  23771  trfil2  23774  flimclslem  23871  fclsrest  23911  fclscf  23912  flimfcls  23913  alexsubALTlem1  23934  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALT  23938  qustgpopn  24007  isxmetd  24214  imasdsf1olem  24261  blcls  24394  prdsxmslem2  24417  metustfbas  24445  dscmet  24460  nrmmetd  24462  reperflem  24707  reconnlem2  24716  xrge0tsms  24723  fsumcn  24761  cnheibor  24854  tcphcph  25137  lmmbr  25158  caubl  25208  ivthlem1  25352  ovolctb  25391  ovoliunlem2  25404  ovolscalem1  25414  ovolicc2  25423  voliunlem3  25453  ismbfd  25540  mbfimaopnlem  25556  itg2le  25640  ellimc2  25778  c1liplem1  25901  plyeq0lem  26115  dgreq0  26171  aannenlem1  26236  pilem2  26362  cxpcn3lem  26657  scvxcvx  26896  musum  27101  fsumdvdsmul  27105  dchrisum0flb  27421  ostth2lem2  27545  sltval2  27568  nolesgn2ores  27584  nogesgn1ores  27586  nosupres  27619  nosupbnd2lem1  27627  noinfres  27634  noinfbnd2lem1  27642  scutun12  27722  madebdayim  27799  precsexlem9  28117  noseqind  28186  zs12bday  28343  numedglnl  29071  upgrreslem  29231  umgrreslem  29232  nbuhgr  29270  nbumgr  29274  uhgrnbgr0nb  29281  nbusgrf1o0  29296  uvtxnbgrvtx  29320  cusgrfilem2  29384  uspgr2wlkeq  29574  wwlks  29765  iswwlksnon  29783  rusgr0edg  29903  clwwlkccatlem  29918  clwwisshclwwslem  29943  clwwlkn  29955  clwwlknon  30019  3cyclfrgrrn  30215  vdgn1frgrv3  30226  2wspmdisj  30266  numclwlk2lem2f1o  30308  frgrregord013  30324  htthlem  30846  ocsh  31212  shintcli  31258  pjss2coi  32093  pjnormssi  32097  pjclem4  32128  pj3si  32136  pj3cor1i  32138  strlem3a  32181  strb  32187  hstrlem3a  32189  hstrbi  32195  spansncv2  32222  mdsl1i  32250  cvmdi  32253  mdexchi  32264  h1da  32278  mdsymlem6  32337  sumdmdii  32344  dmdbr5ati  32351  isoun  32625  xrge0tsmsd  33002  ordtrest2NEW  33913  pwsiga  34120  measiun  34208  dya2iocuni  34274  bnj518  34876  bnj1137  34985  bnj1136  34987  bnj1413  35025  bnj1417  35031  bnj60  35052  gblacfnacd  35089  onvf1odlem1  35090  onvf1odlem4  35093  subgrwlk  35119  erdszelem8  35185  cvmsss2  35261  cvmfolem  35266  fmlasucdisj  35386  satfun  35398  dfon2lem8  35778  dfon2lem9  35779  dfon2  35780  rdgprc  35782  nn0prpwlem  36310  ntruni  36315  clsint2  36317  fneint  36336  fnessref  36345  refssfne  36346  neibastop1  36347  neibastop2lem  36348  bj-0int  37089  bj-ismooredr  37097  relowlpssretop  37352  fvineqsneu  37399  fvineqsneq  37400  heicant  37649  mblfinlem1  37651  ftc2nc  37696  sdclem2  37736  fdc  37739  seqpo  37741  prdsbnd  37787  heibor  37815  rrnequiv  37829  0idl  38019  intidl  38023  unichnidl  38025  prnc  38061  refressn  38434  lsmcv2  39022  lcvexchlem4  39030  lcvexchlem5  39031  eqlkr  39092  paddclN  39836  pclfinN  39894  ldilcnv  40109  ldilco  40110  cdleme25dN  40350  cdlemj2  40816  tendocan  40818  erng1lem  40981  erngdvlem4-rN  40993  dihord2pre  41219  dihglblem2N  41288  dochvalr  41351  hdmap14lem12  41873  hdmap14lem13  41874  supinf  42230  fsuppind  42578  pellfundre  42869  pellfundge  42870  pellfundlb  42872  dford3lem1  43015  aomclem2  43044  oaabsb  43283  cantnf2  43314  ofoafg  43343  naddcnff  43351  naddwordnexlem3  43388  naddwordnexlem4  43390  pwinfi3  43552  iunrelexp0  43691  iunrelexpmin1  43697  iunrelexpmin2  43701  dftrcl3  43709  cnvtrclfv  43713  trclimalb2  43715  dfrtrcl3  43722  ntrneiel2  44075  ntrneik4w  44089  ntrrn  44111  gneispa  44119  gneispb  44120  addrcom  44464  iunconnlem2  44924  ssuzfz  45345  dvnprodlem3  45946  funressnfv  47044  cfsetsnfsetfo  47061  tz6.12-afv  47174  tz6.12-afv2  47241  otiunsndisjX  47280  uniimaprimaeqfv  47383  iccpartltu  47426  iccpartgtl  47427  iccpartleu  47429  iccpartgel  47430  fargshiftf  47441  fargshiftfva  47444  sbgoldbst  47779  bgoldbtbnd  47810  tgblthelfgott  47816  grimuhgr  47887  grimco  47889  isuspgrim0  47894  isuspgrimlem  47895  upgrimpths  47909  gricushgr  47917  grtriclwlk3  47944  stgr0  47959  uspgrlim  47991  grlicsym  48005  nnsgrp  48165  ellcoellss  48424  lindsrng01  48457  suppdm  48499  nn0sumshdiglem1  48610  setrec2fun  49681