Theorem birexdv 1220

Description: Formula-building rule for restricted existential quantifier (deduction rule).

Hypothesis

Ref	Expression
biraldv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
birexdv	|- (ph -> (E.x e. A ps <-> E.x e. A ch))

Distinct variable group(s):   ph,x

Proof of Theorem birexdv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		biraldv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	birexd 1218	1 |- (ph -> (E.x e. A ps <-> E.x e. A ch))

Syntax hints:   -> wi 2   <-> wb 127  E.wrex 1202

This theorem is referenced by:  rexeqd 1328  rcla42ev 1405  eliun 1998  dfiun2 2014  dfiin2 2015  iunrab 2022  iununi 2037  supmo 2156  suplub 2161  freq1 2174  orduninsuc 2365  elima 2606  funcnvuni 2706  fvelima 2859  fvelrn 2883  abrexexlem2 2911  abrexex2 2915  f1oiso 2942  f1oweOLD 2944  tfrlem3 2951  tfrlem12 2960  rdgeq1 2972  rdgeq2 2973  elrnoprab 3054  qseq2 3226  elqs 3227  pssnn 3428  unblem1 3431  unblem2 3432  unbnn2 3436  fiint 3445  tz9.13 3507  aceq1 3552  aceq2 3554  aceq5lem3 3560  aceq5lem4 3561  aceq6a 3564  aceq6b 3565  kmlem8 3587  kmlem11 3590  kmlem14 3593  numth2 3600  numthcor 3601  zornlem7 3609  cardiun 3665  cflim 3704  prnmax 3893  genpv 3896  axrecex 4079  axrnegex 4080  axrrecex 4081  axcnre 4087  nnunb 4520  arch 4521  creur 4532  creui 4533  elq 4629  revalt 4794  imvalt 4795  replimt 4798  clim 4877  clim2 4881  climunii 4883  hcauchy 5103  hlim 5108  hlim2 5112  hlimcaui 5141  hlimunii 5143  chcompl 5150  occllem6 5185  projlem8 5200  projlem10 5202  projlem13 5205  projlem15 5207  projlem17 5209  projlem29 5221  pjtht 5240  pjthu 5241  pjthu2 5242  pjvalt 5246  pjpj0 5259  shsumvalt 5279  shselt 5280  h1de2ct 5461  elspansnt 5471  osumlem5 5534  cvbrt 5714  chrelat2t 5761

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-rex 1206

metamath.org