Metamath Proof Explorer
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 |
⊢ ( 𝐴 ∈ 𝑆 → 𝜓 ) |