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