Theorem ralrimiva 2464

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Assertion

Ref	Expression
ralrimiva	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
2	1	ex 114	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralrimiv 2463	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1448  ∀wral 2375

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380

This theorem is referenced by:  ralrimivvva  2474  rgen2  2477  rgen3  2478  nrexdv  2484  r19.29vva  2535  rabbidva  2629  ssrabdv  3123  ss2rabdv  3125  iuneq2dv  3781  disjeq2dv  3857  mpteq12dva  3949  triun  3979  issod  4179  frirrg  4210  frind  4212  peano2  4447  dmmptd  5189  fun11iun  5322  fniinfv  5411  eqfnfv  5450  eqfnfvd  5453  dff3im  5497  dffo4  5500  fmptd  5506  ffnfv  5510  fmpt2d  5514  ffvresb  5515  fconst2g  5567  fconstfvm  5570  resfunexg  5573  eufnfv  5580  foco2  5587  fniunfv  5595  fcofo  5617  fliftel  5626  fliftfun  5629  fliftfuns  5631  riota5f  5686  grprinvlem  5897  grprinvd  5898  f1ocnvd  5904  suppssov1  5911  offval2  5928  ofrfval2  5929  offveqb  5932  caofref  5934  caofinvl  5935  opabex3d  5950  f1od2  6062  disjxp1  6063  tfrlem1  6135  tfrlemisucaccv  6152  tfrlemiubacc  6157  tfr1onlemsucfn  6167  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemubacc  6173  tfr1onlemaccex  6175  tfr1onlemres  6176  tfrcllemsucfn  6180  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemubacc  6186  tfrcllemaccex  6188  tfrcllemres  6189  tfrcl  6191  rdgon  6213  freccllem  6229  frecfcllem  6231  omcl  6287  oeicl  6288  qliftfuns  6443  ixpeq2dva  6537  xpf1o  6667  mapxpen  6671  isinfinf  6720  fimax2gtrilemstep  6723  undifdcss  6740  eqsuptid  6799  eqinftid  6823  difinfsnlem  6899  difinfsn  6900  ctmlemr  6908  ctm  6909  ctssdclemn0  6910  ctssdclemr  6911  enumctlemm  6913  enomnilem  6922  nnnninf  6935  genprndl  7230  genprndu  7231  nqprloc  7254  ltexprlemrnd  7314  ltexprlemdisj  7315  lteupri  7326  recexprlemrnd  7338  recexprlemdisj  7339  caucvgprlemlim  7390  caucvgprprlemlim  7420  caucvgsrlembound  7489  caucvgsrlemgt1  7490  caucvgsrlemoffgt1  7494  caucvgsr  7497  elrealeu  7517  axcaucvglemcau  7583  axcaucvglemres  7584  negeu  7824  eqord1  8112  eqord2  8113  creur  8575  creui  8576  suprzclex  9001  supinfneg  9240  infsupneg  9241  indstr2  9253  iooidg  9533  iccsupr  9590  icoshftf1o  9615  fznlem  9662  exfzdc  9858  exbtwnzlemstep  9866  exbtwnzlemex  9868  frec2uzrdg  10023  frecuzrdgrcl  10024  frecuzrdgtcl  10026  frecuzrdgsuc  10028  frecuzrdgrclt  10029  frecuzrdgg  10030  frecuzrdgfunlem  10033  frecuzrdgsuctlem  10037  iseqovex  10070  seq3val  10072  seqvalcd  10073  seq3-1  10074  seqf  10075  seq3p1  10076  seqovcd  10077  seqp1cd  10080  seq3clss  10081  seq3fveq2  10083  seq3fveq  10085  seq3feq  10086  seq3shft2  10087  monoord  10090  monoord2  10091  ser3mono  10092  seq3split  10093  seq3caopr3  10095  seq3caopr2  10096  iseqf1olemqk  10108  iseqf1olemjpcl  10109  iseqf1olemqpcl  10110  iseqf1olemfvp  10111  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1oleml  10117  seq3f1o  10118  seq3id3  10121  seq3id  10122  seq3id2  10123  seq3homo  10124  seq3z  10125  ser3ge0  10131  bccl  10354  hashinfuni  10364  hashennnuni  10366  shftf  10443  seq3shft  10451  caucvgrelemcau  10592  cvg1nlemcau  10596  cvg1nlemres  10597  resqrexlemcvg  10631  resqrexlemglsq  10634  resqrexlemga  10635  maxabslemval  10820  negfi  10838  minmax  10840  xrmaxiflemval  10858  xrminmax  10873  climconst  10898  2clim  10909  climcn1  10916  climcn2  10917  reccn2ap  10921  cn1lem  10922  climsqz  10943  climsqz2  10944  climcau  10955  climrecvg1n  10956  serf0  10960  sumeq2dv  10976  sumrbdclem  10984  fsum3cvg  10985  summodclem3  10988  summodclem2a  10989  zsumdc  10992  isum  10993  fsumgcl  10994  fsum3  10995  fsumf1o  10998  isumss  10999  fisumss  11000  isumss2  11001  fsum3cvg2  11002  fsumsersdc  11003  fsum3ser  11005  fsumcl2lem  11006  fsumadd  11014  fsumsplit  11015  fsumm1  11024  fsum1p  11026  isumclim3  11031  isummulc2  11034  sumsplitdc  11040  fsum2dlemstep  11042  fisumcom2  11046  fsumshftm  11053  fsummulc2  11056  fsumge1  11069  fsum00  11070  fsumabs  11073  telfsumo  11074  telfsumo2  11075  fsumparts  11078  fsumrelem  11079  fsumiun  11085  hashiun  11086  hash2iun  11087  binomlem  11091  isumshft  11098  isum1p  11100  isumnn0nn  11101  isumrpcl  11102  isumlessdc  11104  divcnv  11105  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  cvgratnnlemseq  11134  cvgratnnlemabsle  11135  cvgratnnlemfm  11137  cvgratnnlemrate  11138  cvgratnn  11139  cvgratz  11140  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  efcvgfsum  11171  dvdsssfz1  11345  zsupcllemstep  11433  infssuzex  11437  dvdsbnd  11440  bezoutlemstep  11478  bezoutlemmain  11479  bezoutlemle  11489  bezoutlemsup  11490  dfgcd3  11491  dfgcd2  11495  coprmgcdb  11562  isprm6  11618  phivalfi  11680  phibndlem  11684  dfphi2  11688  hashdvds  11689  phiprmpw  11690  phimullem  11693  hashgcdeq  11696  ennnfonelemex  11719  ennnfonelemfun  11722  ennnfonelemf1  11723  ennnfonelemnn0  11727  ennnfonelemim  11729  exmidunben  11731  ctinfomlemom  11732  ctinfom  11733  ctinf  11735  fiinbas  11998  tgclb  12016  restbasg  12119  iscnp4  12168  cnco  12171  cnptopco  12172  cnss1  12176  cnss2  12177  cncnpi  12178  cncnp  12180  cnconst2  12183  cnrest  12185  cnptopresti  12188  cnpdis  12192  lmtopcnp  12200  txbasval  12217  tx1cn  12219  tx2cn  12220  txcnp  12221  upxp  12222  txdis1cn  12228  cnmpt11  12233  psmet0  12255  psmettri2  12256  psmetxrge0  12260  psmetres2  12261  ismeti  12274  xmetpsmet  12297  blsscls2  12421  comet  12427  tgioo  12465  tgqioo  12466  elcncf1di  12479  cdivcncfap  12499  mulcncflem  12502  mulcncf  12503  nnsf  12783  nninfalllemn  12786  nninfalllem1  12787  nninfall  12788  nninfself  12793  nninfsellemeq  12794  nninfsellemeqinf  12796  nninfsel  12797  isomninnlem  12809  trilpolemeq1  12817  trilpo  12820