Theorem rexbiia 1721

Description: Inference adding restricted existential quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
ralbiia.1	⊢ (x ∈ A → (φ ↔ ψ))

Assertion

Ref	Expression
rexbiia	⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Proof of Theorem rexbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 ⊢ (x ∈ A → (φ ↔ ψ))
2	1	pm5.32i 656	. 2 ⊢ ((x ∈ A ⋀ φ) ↔ (x ∈ A ⋀ ψ))
3	2	rexbii2 1719	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Syntax hints:   → wi 3   ↔ wb 153   ∈ wcel 999  ∃wrex 1693

This theorem is referenced by:  2rexbiia 1722  reu8 1983  f1oweALT 3964  unbndrank 4745  infm3 6136  reeff1o 7517  efghgrpilem 8802  efifo 8812  projlemHIL 9301  pjpj0i 9338  nmopnegi 9972  nmop0 9993  nmfn0 9994  adjbd1o 10101  atom1d 10364

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-rex 1697

Copyright terms: Public domain