Step |
Hyp |
Ref |
Expression |
1 |
|
sbcex |
⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) → 𝐴 ∈ V ) |
2 |
|
sbcex |
⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V ) |
3 |
|
sbcex |
⊢ ( [ 𝐴 / 𝑥 ] 𝜓 → 𝐴 ∈ V ) |
4 |
2 3
|
jaoi |
⊢ ( ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) → 𝐴 ∈ V ) |
5 |
|
dfsbcq2 |
⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ) ) |
6 |
|
dfsbcq2 |
⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) ) |
7 |
|
dfsbcq2 |
⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ [ 𝐴 / 𝑥 ] 𝜓 ) ) |
8 |
6 7
|
orbi12d |
⊢ ( 𝑦 = 𝐴 → ( ( [ 𝑦 / 𝑥 ] 𝜑 ∨ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) ) ) |
9 |
|
sbor |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∨ [ 𝑦 / 𝑥 ] 𝜓 ) ) |
10 |
5 8 9
|
vtoclbg |
⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) ) ) |
11 |
1 4 10
|
pm5.21nii |
⊢ ( [ 𝐴 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝐴 / 𝑥 ] 𝜑 ∨ [ 𝐴 / 𝑥 ] 𝜓 ) ) |