Theorem 2sbcrexOLD

Description: Exchange an existential quantifier with two substitutions. (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
Hypotheses	2sbcrex.1	⊢ 𝐴 ∈ V
	2sbcrex.2	⊢ 𝐵 ∈ V
Assertion	2sbcrexOLD	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		2sbcrex.1	⊢ 𝐴 ∈ V
2		2sbcrex.2	⊢ 𝐵 ∈ V
3		sbcrexgOLD	⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑏 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐵 / 𝑏 ] 𝜑 ) )
4	2 3	ax-mp	⊢ ( [ 𝐵 / 𝑏 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐵 / 𝑏 ] 𝜑 )
5	4	sbcbii	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 [ 𝐵 / 𝑏 ] 𝜑 )
6		sbcrexgOLD	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 [ 𝐵 / 𝑏 ] 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 ) )
7	1 6	ax-mp	⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 [ 𝐵 / 𝑏 ] 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 )
8	5 7	bitri	⊢ ( [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] [ 𝐵 / 𝑏 ] 𝜑 )