Theorem rexlimiv 3126

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

Hypothesis

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

Assertion

Ref	Expression
rexlimiv	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

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

Proof of Theorem rexlimiv

Step	Hyp	Ref	Expression
1		rexlimiv.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
2	1	imp 406	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3125	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rexlimdv  3131  rexlimivv  3174  issn  4784  uniss2  4892  disjiun  5079  reuop  6240  ssimaex  6907  ordzsl  7775  onzsl  7776  mpoexw  8010  fsplitfpar  8048  tfrlem8  8303  nneob  8571  ecoptocl  8731  elixpsn  8861  ixpsnf1o  8862  findcard  9073  findcard2  9074  ssfiALT  9083  php  9116  php3  9118  ordunifi  9174  fiint  9211  en3lp  9504  inf0  9511  inf3lemd  9517  inf3lem6  9523  noinfep  9550  cantnfvalf  9555  dmttrcl  9611  rnttrcl  9612  ttrclselem1  9615  trcl  9618  bndrank  9734  rankc2  9764  tcrank  9777  ficardom  9854  ac10ct  9925  isinfcard  9983  alephfp  9999  dfac5lem4  10017  dfac5lem4OLD  10019  dfac2b  10022  ackbij2  10133  fin23lem16  10226  fin23lem29  10232  fin17  10285  fin1a2lem6  10296  itunitc  10312  hsmexlem9  10316  axdc3lem2  10342  axdc3lem4  10344  axcclem  10348  zorn2lem7  10393  wunr1om  10610  tskr1om  10658  grothomex  10720  prnmadd  10888  ltaprlem  10935  mulgt0sr  10996  0cnALT2  11349  renegcli  11422  peano2nn  12137  bndndx  12380  uzn0  12749  ublbneg  12831  om2uzrani  13859  uzrdgfni  13865  exprelprel  14397  rtrclreclem3  14967  rtrclind  14972  rexanuz2  15257  caurcvg  15584  caucvg  15586  infcvgaux1i  15764  vdwlem6  16898  dfgrp2e  18876  efgrelexlemb  19663  pzriprnglem5  21423  pzriprnglem6  21424  pzriprnglem12  21430  cygth  21509  psgnghm  21518  iscldtop  23011  opnneiid  23042  pnfnei  23136  mnfnei  23137  discmp  23314  cmpsublem  23315  cmpfi  23324  2ndcredom  23366  2ndc1stc  23367  2ndcdisj  23372  kgenidm  23463  methaus  24436  xrtgioo  24723  caun0  25209  ovolmge0  25406  itg2lcl  25656  aannenlem2  26265  aannenlem3  26266  aaliou2  26276  2lgslem1b  27331  2sqlem2  27357  ostth  27578  nodmon  27590  sltval2  27596  bdayfo  27617  madef  27798  addsprop  27920  negsprop  27978  mulsprop  28070  elons2  28196  nnsge1  28272  onsfi  28284  dfnns2  28298  n0seo  28345  0reno  28400  remulscllem1  28403  midwwlks2s3  29931  3cyclfrgrrn1  30263  3cyclfrgrrn  30264  h1de2ctlem  31533  h1de2ci  31534  spansni  31535  spanunsni  31557  riesz3i  32040  adjbd1o  32063  rnbra  32085  pjnmopi  32126  dfpjop  32160  atom1d  32331  cvexchlem  32346  cdj1i  32411  cdj3lem1  32412  hasheuni  34096  cvmlift2lem12  35356  satfrnmapom  35412  sat1el2xp  35421  fmla1  35429  gonar  35437  goalr  35439  fmla0disjsuc  35440  mrsubccat  35560  msrid  35587  elmthm  35618  untint  35754  nnuni  35769  dfon2lem3  35825  dfon2lem7  35829  dfrdg2  35835  finminlem  36358  fneint  36388  ptrecube  37666  poimirlem26  37692  poimirlem27  37693  poimirlem29  37695  poimirlem30  37696  zerdivemp1x  37993  dochsnnz  41495  ismrc  42740  eldiophb  42796  eldioph4b  42850  dfacbasgrp  43147  dfsucon  43562  orbitcl  44996  subsaliuncllem  46401  icoresmbl  46587  elsetpreimafvssdm  47423  sprsymrelfvlem  47527  sprsymrelf1lem  47528  prmdvdsfmtnof1lem2  47622  isgrtri  47980  stgredgel  47994  stgr1  47998  uspgropssxp  48181  0aryfvalel  48672