Theorem rexbidva 1663

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

Hypothesis

Ref	Expression
ralbidva.1	⊢ ((φ ⋀ x ∈ A) → (ψ ↔ χ))

Assertion

Ref	Expression
rexbidva	⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Distinct variable group:   φ,x

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 ⊢ (φ → ∀xφ)
2		ralbidva.1	. 2 ⊢ ((φ ⋀ x ∈ A) → (ψ ↔ χ))
3	1, 2	rexbida 1661	1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ∈ wcel 960  ∃wrex 1649

This theorem is referenced by:  2rexbiia 1678  2rexbidva 1682  weinxp 3239  dfimafn 3767  funimass4 3769  fvelimab 3771  fconstfv 3855  isomin 3905  f1oiso 3910  oaass 4201  r1pwcl 4697  brdom7disj 4814  brdom6disj 4815  cnegextlem3 5359  axsup 5519  sup3 6054  infm3 6056  infmsup 6070  nnreclt 6074  supxrre 6085  supxrbnd 6093  supxrbnd1 6097  supxrbnd2 6098  expnlbndt 6656  cau2 6913  sumeq2 6985  infcvglem1 7221  qdensere 7748  iscnp2 7758  cncnplem4 7774  blrn3 7844  metcnplem 7883  metcnp3 7893  iscauf 7936  iscau5 7938  iscaunns 7941  causs 7952  cncms 7995  bcthlem21 8016  nmounbi 8435  nmo0 8447  minveclem28 8568  efifolem7 8723  hcau2 9050  hhcms 9067  hhsscms 9145  projlem1 9181  projlem2 9182  projlem26 9206  pjtheu2 9245  shsel3t 9274  branmfnt 10033  pjima 10099  chrelat 10286  cdj3lem3 10360  cdj3lem3b 10362  fgsb 10555  fgsb2 10560

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain