Metamath Proof Explorer

Theorem 2sbcrex

Description: Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by NM, 24-Aug-2018)

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

Proof

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