Theorem rexlimddv 2673

Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
rexlimddv.1	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
rexlimddv.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)

Assertion

Ref	Expression
rexlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

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

Proof of Theorem rexlimddv

Step	Hyp	Ref	Expression
1		rexlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		rexlimddv.2	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3	2	rexlimdvaa 2669	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∃wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is used by:  disjiun  4125  nnsucpred  4764  tfrlemisucaccv  6596  tfrexlem  6605  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  fict  7170  fidceq  7171  dif1enen  7184  php5fin  7186  fisbth  7187  fin0  7189  fin0or  7190  diffisn  7197  infnfi  7199  fidcen  7203  fientri3  7222  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  fiuni  7312  ctmlemr  7449  ctssdccl  7452  fodjum  7487  fodju0  7488  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  cc2lem  7633  prarloclemarch2  7787  addlocpr  7904  nqprl  7919  nqpru  7920  appdiv0nq  7932  prmuloc  7934  mullocpr  7939  ltprordil  7957  ltaddpr  7965  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  ltaprlem  7986  ltaprg  7987  prplnqu  7988  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  ltmprr  8010  archpr  8011  cauappcvgprlemopl  8014  cauappcvgprlemopu  8016  cauappcvgprlemloc  8020  cauappcvgprlem1  8027  cauappcvgprlem2  8028  archrecpr  8032  caucvgprlemopl  8037  caucvgprlemopu  8039  caucvgprlemloc  8043  caucvgprlem2  8048  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemopl  8065  caucvgprprlemopu  8067  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocexprlemrl  8085  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemloc  8089  suplocexprlemex  8090  suplocexprlemub  8091  suplocexprlemlub  8092  prsrriota  8156  caucvgsrlemgt1  8163  caucvgsrlemoffres  8168  suplocsrlem  8176  rereceu  8257  recriota  8258  axarch  8259  axcaucvglemres  8267  axpre-suploclemres  8269  readdcan  8468  cnegex  8506  addcan  8508  addcan2  8509  negeu  8519  ltadd2  8749  recexre  8909  rimul  8916  ltmul1  8923  mulap0  8985  mulcanapd  8992  suprzclex  9749  zsupcllemex  10674  zssinfcl  10676  suprzubdc  10682  zsupssdc  10684  suprzcl2dc  10685  qbtwnre  10702  hashcl  11236  hashen  11239  fihashdom  11259  hashunlem  11260  hashun  11261  zfz1iso  11309  lencl  11324  sswrd  11329  cvg1nlemres  11767  cvg1n  11768  recvguniq  11777  resqrexlemoverl  11803  resqrexlemex  11807  fimaxre2  12010  climge0  12110  climrecvg1n  12133  fsum3cvg3  12182  expcnvre  12289  mertenslemub  12320  efcllem  12445  oexpneg  12663  bitsfzolem  12740  bitsfi  12743  bezoutlemnewy  12792  bezoutlemstep  12793  dfgcd3  12806  bezout  12807  isprm5lem  12939  ballotfilemscl  13299  ballotfilemsle  13300  ennnfonelemex  13357  ennnfonelemrnh  13359  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemdm  13363  ennnfonelemnn0  13365  ctinfomlemom  13370  ctinf  13373  ctiunctlemfo  13382  nninfdclemcl  13391  nninfdc  13396  grpinvalem  13758  grprida  13760  grprcan  13895  psrbaglefifi  15147  mplsubgfilemcl  15181  restbasg  15360  cnpnei  15411  cnptopco  15414  xmettx  15702  metcnpi3  15709  mulcncf  15800  dedekindeulemuub  15809  dedekindeulemub  15810  dedekindeulemlu  15813  dedekindicclemuub  15818  dedekindicclemub  15819  dedekindicclemlu  15822  dedekindicc  15825  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthreinc  15837  ivthdichlem  15843  limcimolemlt  15856  limcimo  15857  limccnp2cntop  15869  reeff1oleme  15964  eflt  15967  upgredg  16551  bj-charfunr  17002  qdencn  17238  trilpolemlt1  17257  nconstwlpolemgt0  17281