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

Metamath Proof Explorer

Theorem sbcan

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

Ref Expression
Assertion sbcan ⊢ [˙A / x]˙ φ ∧ ψ ↔ [˙A / x]˙ φ ∧ [˙A / x]˙ ψ

Proof

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