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 | ⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcrex | ⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ) | |
2 | sbcrex | ⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) | |
3 | 2 | rexbii | ⊢ ( ∃ 𝑏 ∈ 𝐵 [ 𝐴 / 𝑎 ] ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) |
4 | 1 3 | bitri | ⊢ ( [ 𝐴 / 𝑎 ] ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝜑 ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 [ 𝐴 / 𝑎 ] 𝜑 ) |