Metamath Proof Explorer


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 ( [ 𝐴 / 𝑎 ]𝑏𝐵𝑐𝐶 𝜑 ↔ ∃ 𝑏𝐵𝑐𝐶 [ 𝐴 / 𝑎 ] 𝜑 )