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

Metamath Proof Explorer

Theorem ectocl

Description: Implicit substitution of class for equivalence class. (Contributed by NM, 23-Jul-1995) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypotheses ectocl.1 ⊢ S = B / R
ectocl.2 ⊢ x R = A → φ ↔ ψ
ectocl.3 ⊢ x ∈ B → φ
Assertion ectocl ⊢ A ∈ S → ψ

Proof

Step Hyp Ref Expression
1 ectocl.1 ⊢ S = B / R
2 ectocl.2 ⊢ x R = A → φ ↔ ψ
3 ectocl.3 ⊢ x ∈ B → φ
4 tru ⊢ ⊤
5 3 adantl ⊢ ⊤ ∧ x ∈ B → φ
6 1 2 5 ectocld ⊢ ⊤ ∧ A ∈ S → ψ
7 4 6 mpan ⊢ A ∈ S → ψ