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

Metamath Proof Explorer

Theorem sbbi

Description: Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993)

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

Proof

Step Hyp Ref Expression
1 dfbi2 ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) )
2 1 sbbii ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜓 ) ↔ [ 𝑦 / 𝑥 ] ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) )
3 sbim ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )
4 sbim ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜑 ) )
5 3 4 anbi12i ⊢ ( ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜑 ) ) ↔ ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
6 sban ⊢ ( [ 𝑦 / 𝑥 ] ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ∧ [ 𝑦 / 𝑥 ] ( 𝜓 → 𝜑 ) ) )
7 dfbi2 ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ∧ ( [ 𝑦 / 𝑥 ] 𝜓 → [ 𝑦 / 𝑥 ] 𝜑 ) ) )
8 5 6 7 3bitr4i ⊢ ( [ 𝑦 / 𝑥 ] ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )
9 2 8 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )