Metamath Proof Explorer

Theorem sbc4rex

Description: Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

Ref Expression
Assertion sbc4rex ⊢ [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ

Proof

Step Hyp Ref Expression
1 sbc2rex ⊢ [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ
2 sbc2rex ⊢ [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ
3 2 2rexbii ⊢ ∃ b ∈ B ∃ c ∈ C [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ
4 1 3 bitri ⊢ [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ