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 ( 𝐴𝑆𝜓 )