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

Metamath Proof Explorer

Theorem ecoptocl

Description: Implicit substitution of class for equivalence class of ordered pair. (Contributed by NM, 23-Jul-1995)

Ref Expression
Hypotheses ecoptocl.1 ⊢ 𝑆 = ( ( 𝐵 × 𝐶 ) / 𝑅 )
ecoptocl.2 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ecoptocl.3 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝜑 )
Assertion ecoptocl ( 𝐴 ∈ 𝑆 → 𝜓 )

Proof

Step Hyp Ref Expression
1 ecoptocl.1 ⊢ 𝑆 = ( ( 𝐵 × 𝐶 ) / 𝑅 )
2 ecoptocl.2 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3 ecoptocl.3 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝜑 )
4 elqsi ⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) / 𝑅 ) → ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) 𝐴 = [ 𝑧 ] 𝑅 )
5 eqid ⊢ ( 𝐵 × 𝐶 ) = ( 𝐵 × 𝐶 )
6 eceq1 ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = [ 𝑧 ] 𝑅 )
7 6 eqeq2d ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ( 𝐴 = [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 ↔ 𝐴 = [ 𝑧 ] 𝑅 ) )
8 7 imbi1d ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝑧 → ( ( 𝐴 = [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 → 𝜓 ) ↔ ( 𝐴 = [ 𝑧 ] 𝑅 → 𝜓 ) ) )
9 2 eqcoms ⊢ ( 𝐴 = [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 → ( 𝜑 ↔ 𝜓 ) )
10 3 9 syl5ibcom ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → ( 𝐴 = [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 → 𝜓 ) )
11 5 8 10 optocl ⊢ ( 𝑧 ∈ ( 𝐵 × 𝐶 ) → ( 𝐴 = [ 𝑧 ] 𝑅 → 𝜓 ) )
12 11 rexlimiv ⊢ ( ∃ 𝑧 ∈ ( 𝐵 × 𝐶 ) 𝐴 = [ 𝑧 ] 𝑅 → 𝜓 )
13 4 12 syl ⊢ ( 𝐴 ∈ ( ( 𝐵 × 𝐶 ) / 𝑅 ) → 𝜓 )
14 13 1 eleq2s ⊢ ( 𝐴 ∈ 𝑆 → 𝜓 )