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	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 [ 𝐴 / 𝑎 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbc2rex	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 )
2		sbc2rex	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 ↔ ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 [ 𝐴 / 𝑎 ] 𝜑 )
3	2	2rexbii	⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 [ 𝐴 / 𝑎 ] 𝜑 )
4	1 3	bitri	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 ∃ 𝑒 ∈ 𝐸 [ 𝐴 / 𝑎 ] 𝜑 )