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 ⊢ 𝑆 = ( 𝐵 / 𝑅 )
ectocl.2 ⊢ ( [ 𝑥 ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ectocl.3 ⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
Assertion ectocl ( 𝐴 ∈ 𝑆 → 𝜓 )

Proof

Step Hyp Ref Expression
1 ectocl.1 ⊢ 𝑆 = ( 𝐵 / 𝑅 )
2 ectocl.2 ⊢ ( [ 𝑥 ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 ectocl.3 ⊢ ( 𝑥 ∈ 𝐵 → 𝜑 )
4 tru ⊢ ⊤
5 3 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
6 1 2 5 ectocld ⊢ ( ( ⊤ ∧ 𝐴 ∈ 𝑆 ) → 𝜓 )
7 4 6 mpan ⊢ ( 𝐴 ∈ 𝑆 → 𝜓 )