Metamath Proof Explorer

Theorem sbc4rexgOLD

Description: Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014) Obsolete as of 24-Aug-2018. Use csbov123 instead. (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion sbc4rexgOLD ⊢ A ∈ V → [˙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 elex ⊢ A ∈ V → A ∈ V
2 sbc2rexgOLD ⊢ A ∈ V → [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ
3 sbc2rexgOLD ⊢ A ∈ V → [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ
4 3 2rexbidv ⊢ A ∈ V → ∃ b ∈ B ∃ c ∈ C [˙A / a]˙ ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ
5 2 4 bitrd ⊢ A ∈ V → [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ
6 1 5 syl ⊢ A ∈ V → [˙A / a]˙ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E φ ↔ ∃ b ∈ B ∃ c ∈ C ∃ d ∈ D ∃ e ∈ E [˙A / a]˙ φ