Metamath Proof Explorer

Theorem sbcor

Description: Distribution of class substitution over disjunction. (Contributed by NM, 31-Dec-2016) (Revised by NM, 17-Aug-2018)

Ref Expression
Assertion sbcor ⊢ [˙A / x]˙ φ ∨ ψ ↔ [˙A / x]˙ φ ∨ [˙A / x]˙ ψ

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ φ ∨ ψ → A ∈ V
2 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
3 sbcex ⊢ [˙A / x]˙ ψ → A ∈ V
4 2 3 jaoi ⊢ [˙A / x]˙ φ ∨ [˙A / x]˙ ψ → A ∈ V
5 dfsbcq2 ⊢ y = A → y x φ ∨ ψ ↔ [˙A / x]˙ φ ∨ ψ
6 dfsbcq2 ⊢ y = A → y x φ ↔ [˙A / x]˙ φ
7 dfsbcq2 ⊢ y = A → y x ψ ↔ [˙A / x]˙ ψ
8 6 7 orbi12d ⊢ y = A → y x φ ∨ y x ψ ↔ [˙A / x]˙ φ ∨ [˙A / x]˙ ψ
9 sbor ⊢ y x φ ∨ ψ ↔ y x φ ∨ y x ψ
10 5 8 9 vtoclbg ⊢ A ∈ V → [˙A / x]˙ φ ∨ ψ ↔ [˙A / x]˙ φ ∨ [˙A / x]˙ ψ
11 1 4 10 pm5.21nii ⊢ [˙A / x]˙ φ ∨ ψ ↔ [˙A / x]˙ φ ∨ [˙A / x]˙ ψ