Description: Exchange a substitution with two existentials. (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 | ||
|---|---|---|---|
| Assertion | sbc2rexgOLD | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elex | ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) | |
| 2 | sbcrexgOLD | ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ) ) | |
| 3 | sbcrexgOLD | ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) ) | |
| 4 | 3 | rexbidv | ⊢ ( 𝐴 ∈ V → ( ∃ 𝑏 ∈ 𝐵 [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) ) |
| 5 | 2 4 | bitrd | ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) ) |
| 6 | 1 5 | syl | ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) ) |