This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbor

Description: Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002)

Ref Expression
Assertion sbor ( [ 𝑦 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∨ [ 𝑦 / 𝑥 ] 𝜓 ) )

Proof

Step Hyp Ref Expression
1 sbim ⊢ ( [ 𝑦 / 𝑥 ] ( ¬ 𝜑 → 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
2 sbn ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 )
3 2 imbi1i ⊢ ( ( [ 𝑦 / 𝑥 ] ¬ 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( ¬ [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
4 1 3 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
5 df-or ⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 → 𝜓 ) )
6 5 sbbii ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ [ 𝑦 / 𝑥 ] ( ¬ 𝜑 → 𝜓 ) )
7 df-or ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ∨ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( ¬ [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
8 4 6 7 3bitr4i ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ∨ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ∨ [ 𝑦 / 𝑥 ] 𝜓 ) )