Theorem sbc2rex

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

	Ref	Expression
Assertion	sbc2rex	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 )

Proof

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