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  7448  ctssdccl  7451  fodjum  7486  fodju0  7487  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  cc2lem  7632  prarloclemarch2  7786  addlocpr  7903  nqprl  7918  nqpru  7919  appdiv0nq  7931  prmuloc  7933  mullocpr  7938  ltprordil  7956  ltaddpr  7964  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemloc  7974  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  ltaprlem  7985  ltaprg  7986  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  ltmprr  8009  archpr  8010  cauappcvgprlemopl  8013  cauappcvgprlemopu  8015  cauappcvgprlemloc  8019  cauappcvgprlem1  8026  cauappcvgprlem2  8027  archrecpr  8031  caucvgprlemopl  8036  caucvgprlemopu  8038  caucvgprlemloc  8042  caucvgprlem2  8047  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemopu  8066  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemex  8089  suplocexprlemub  8090  suplocexprlemlub  8091  prsrriota  8155  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  suplocsrlem  8175  rereceu  8256  recriota  8257  axarch  8258  axcaucvglemres  8266  axpre-suploclemres  8268  readdcan  8466  cnegex  8504  addcan  8506  addcan2  8507  negeu  8517  ltadd2  8747  recexre  8906  rimul  8913  ltmul1  8920  mulap0  8982  mulcanapd  8989  suprzclex  9744  zsupcllemex  10663  zssinfcl  10665  suprzubdc  10671  zsupssdc  10673  suprzcl2dc  10674  qbtwnre  10691  hashcl  11220  hashen  11223  fihashdom  11243  hashunlem  11244  hashun  11245  zfz1iso  11293  lencl  11308  sswrd  11313  cvg1nlemres  11751  cvg1n  11752  recvguniq  11761  resqrexlemoverl  11787  resqrexlemex  11791  fimaxre2  11993  climge0  12091  climrecvg1n  12114  fsum3cvg3  12163  expcnvre  12270  mertenslemub  12301  efcllem  12426  oexpneg  12644  bitsfzolem  12721  bitsfi  12724  bezoutlemnewy  12773  bezoutlemstep  12774  dfgcd3  12787  bezout  12788  isprm5lem  12919  ballotfilemscl  13247  ballotfilemsle  13248  ennnfonelemex  13305  ennnfonelemrnh  13307  ennnfonelemf1  13309  ennnfonelemrn  13310  ennnfonelemdm  13311  ennnfonelemnn0  13313  ctinfomlemom  13318  ctinf  13321  ctiunctlemfo  13330  nninfdclemcl  13339  nninfdc  13344  grpinvalem  13705  grprida  13707  grprcan  13842  mplsubgfilemcl  15090  restbasg  15269  cnpnei  15320  cnptopco  15323  xmettx  15611  metcnpi3  15618  mulcncf  15709  dedekindeulemuub  15718  dedekindeulemub  15719  dedekindeulemlu  15722  dedekindicclemuub  15727  dedekindicclemub  15728  dedekindicclemlu  15731  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthreinc  15746  ivthdichlem  15752  limcimolemlt  15765  limcimo  15766  limccnp2cntop  15778  reeff1oleme  15873  eflt  15876  upgredg  16385  bj-charfunr  16836  qdencn  17072  trilpolemlt1  17090  nconstwlpolemgt0  17114