Theorem rexlimdv 3132

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2020.)

Hypothesis

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

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

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

Proof of Theorem rexlimdv

Step	Hyp	Ref	Expression
1		rexlimdv.1	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
2	1	com3l 89	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜓 → (𝜑 → 𝜒)))
3	2	rexlimiv 3127	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 → (𝜑 → 𝜒))
4	3	com12 32	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3057

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 3058

This theorem is referenced by:  rexlimdva  3134  rexlimdva2  3136  rexlimdv3a  3138  rexlimdvw  3139  rexlimdvv  3189  rexlimdvvva  3191  elpwunsn  4638  onelssex  6362  eldmrexrnb  7033  weniso  7296  ssorduni  7720  onint  7731  limuni3  7790  peano5  7831  funcnvuni  7870  funeldmdif  7988  frxp  8064  smoiun  8289  tfrlem9  8312  oaordex  8481  oalimcl  8483  oaass  8484  findcard2  9083  findcard3  9176  frfi  9178  unblem1  9185  ordiso2  9410  inf3lem3  9529  r1sdom  9676  tz9.12lem3  9691  karden  9797  infxpenlem  9913  cardinfima  9997  iunfictbso  10014  dfac5  10029  cfcoflem  10172  fin23lem11  10217  fin23lem30  10242  fin1a2lem13  10312  axdc3lem2  10351  konigthlem  10468  fpwwe2lem11  10541  tskuni  10683  axgroth6  10728  nqereu  10829  genpnmax  10907  ltaddpr  10934  recexsrlem  11003  mulgt0sr  11005  axrrecex  11063  axpre-sup  11069  addrid  11302  addlid  11305  recex  11758  btwnz  12584  lbzbi  12838  qbtwnre  13102  caubnd  15270  divalglem9  16316  unbenlem  16824  firest  17340  imasmnd2  18686  imasgrp2  18972  pmtrfrn  19374  pgpfi  19521  sylow2blem3  19538  imasrng  20099  imasring  20252  lspsneq  21063  lspdisj  21066  elcls  22991  elcls3  23001  subbascn  23172  cmpsublem  23317  cmpsub  23318  nllyidm  23407  comppfsc  23450  ptpjopn  23530  fbfinnfr  23759  filin  23772  isfil2  23774  infil  23781  fgss2  23792  fgfil  23793  fgcl  23796  fgabs  23797  elfm2  23866  rnelfm  23871  fmfnfmlem2  23873  fmfnfmlem4  23875  fmco  23879  flffbas  23913  cnpflf2  23918  fclscf  23943  alexsubALTlem2  23966  alexsubALTlem3  23967  alexsubALTlem4  23968  alexsubALT  23969  neibl  24419  met2ndc  24441  metcnp3  24458  icccmplem2  24742  xrge0tsms  24753  fgcfil  25201  volfiniun  25478  dyadmax  25529  dyadmbllem  25530  c1liplem1  25931  dgrlem  26164  axcontlem10  28955  usgredg2vtxeuALT  29204  ushgredgedg  29211  ushgredgedgloop  29213  uhgrspan1  29285  nbuhgr2vtx1edgblem  29333  erclwwlksym  30005  erclwwlknsym  30054  1pthon2v  30137  conngrv2edg  30179  lpni  30464  grpoidinvlem3  30490  grporcan  30502  omlsii  31387  spansncol  31552  spansnss  31555  spanunsni  31563  h1datomi  31565  nmopsetretALT  31847  branmfn  32089  chjatom  32341  cvbr4i  32351  atomli  32366  xrge0tsmsd  33051  umgr2cycllem  35207  umgr2cycl  35208  sat1el2xp  35446  fmlasuc  35453  satffunlem1lem2  35470  satffunlem2lem1  35471  satffunlem2lem2  35473  dfon2lem6  35853  colineardim1  36128  finminlem  36385  nn0prpwlem  36389  neibastop2lem  36427  neibastop2  36428  fgmin  36437  exrecfnlem  37446  heiborlem10  37883  prtlem15  38997  lshpcmp  39110  lsatn0  39121  lsatcmp  39125  lsmsat  39130  lsatcv0  39153  l1cvpat  39176  eqlkr  39221  lshpkrlem1  39232  lshpkrlem6  39237  lfl1dim  39243  lfl1dim2N  39244  lkrss2N  39291  athgt  39578  3dim2  39590  llnle  39640  llncmp  39644  lplnle  39662  lplnnle2at  39663  llncvrlpln2  39679  llncvrlpln  39680  lplncmp  39684  lplnexllnN  39686  lvolnle3at  39704  lplncvrlvol2  39737  lplncvrlvol  39738  lvolcmp  39739  pointpsubN  39873  pclfinN  40022  pclfinclN  40072  osumcllem11N  40088  pexmidlem4N  40095  cdleme17d3  40618  cdlemeg46gfre  40654  cdleme48gfv1  40658  cdleme50trn2  40673  trlord  40691  cdlemg6e  40744  cdlemj3  40945  diaelrnN  41167  diaintclN  41180  dia2dimlem6  41191  cdlemm10N  41240  dibintclN  41289  dihord6apre  41378  dihord5b  41381  dihord5apre  41384  dihglblem5apreN  41413  dihglblem2N  41416  dihglblem3N  41417  dihglbcpreN  41422  dihintcl  41466  lclkrlem2y  41653  lcfrvalsnN  41663  isnacs3  42830  jm2.26  43122  fnwe2lem2  43171  hbtlem5  43248  dflim5  43449  uzwo4  45177  iunincfi  45218  restuni3  45242  disjinfi  45316  ssnnf1octb  45318  choicefi  45324  mapssbi  45337  unirnmapsn  45338  iunmapsn  45341  supxrgere  45459  supxrgelem  45463  suplesup  45465  infleinf  45497  suplesup2  45501  rexabslelem  45543  islptre  45746  limcperiod  45755  limclner  45776  limsupmnfuzlem  45851  limsupre3lem  45857  coskpi2  45991  cosknegpi  45994  icccncfext  46012  stoweidlem27  46152  stoweidlem59  46184  fourierdlem41  46273  fourierdlem42  46274  fourierdlem70  46301  fourierdlem71  46302  fourierdlem81  46312  fourierswlem  46355  qndenserrnopnlem  46422  subsaliuncl  46483  subsalsal  46484  sge0tsms  46505  sge0fsum  46512  sge0supre  46514  sge0sup  46516  sge0rnbnd  46518  sge0pnffigt  46521  sge0resrn  46529  sge0split  46534  sge0iunmptlemfi  46538  sge0rpcpnf  46546  sge0isum  46552  sge0xaddlem2  46559  sge0uzfsumgt  46569  sge0seq  46571  sge0reuz  46572  nnfoctbdjlem  46580  nnfoctbdj  46581  meadjiunlem  46590  meaiuninclem  46605  carageniuncllem2  46647  caratheodorylem2  46652  ovnsupge0  46682  ovncvrrp  46689  hoidmv1lelem3  46718  hoidmv1le  46719  hoidmvlelem1  46720  hoidmvlelem2  46721  hoidmvlelem3  46722  ovnhoilem2  46727  opnvonmbllem2  46758  ovnovollem3  46783  sssmf  46863  smfpimbor1lem1  46923  smfco  46927  smfpimcc  46933  smfinflem  46942  fmtno4prmfac  47699  sfprmdvdsmersenne  47730  nnsum4primeseven  47927  nnsum4primesevenALTV  47928  bgoldbtbnd  47936  grimuhgr  48014  clnbgrgrim  48061  uspgrlimlem2  48116