Theorem rexbi

Description: Distribute restricted quantification over a biconditional. (Contributed by Scott Fenton, 7-Aug-2024) (Proof shortened by Wolf Lammen, 3-Nov-2024)

	Ref	Expression
Assertion	rexbi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) )
3		rexim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
4	2 3	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 𝜓 ) )
5		biimpr	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜓 → 𝜑 ) )
6	5	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) )
7		rexim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
8	6 7	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 𝜑 ) )
9	4 8	impbid	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜓 ) )