ecoptocl

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

Step	Hyp	Ref	Expression
1		ecoptocl.1	$⊢ S = (B \times C) / R$
2		ecoptocl.2	$⊢ [⟨x, y⟩] R = A \to (φ \leftrightarrow ψ)$
3		ecoptocl.3	$⊢ (x \in B \land y \in C) \to φ$
4		elqsi	$⊢ A \in ((B \times C) / R) \to \exists z \in (B \times C) A = [z] R$
5		eqid	$⊢ B \times C = B \times C$
6		eceq1	$⊢ ⟨x, y⟩ = z \to [⟨x, y⟩] R = [z] R$
7	6	eqeq2d	$⊢ ⟨x, y⟩ = z \to (A = [⟨x, y⟩] R \leftrightarrow A = [z] R)$
8	7	imbi1d	$⊢ ⟨x, y⟩ = z \to ((A = [⟨x, y⟩] R \to ψ) \leftrightarrow (A = [z] R \to ψ))$
9	2	eqcoms	$⊢ A = [⟨x, y⟩] R \to (φ \leftrightarrow ψ)$
10	3 9	syl5ibcom	$⊢ (x \in B \land y \in C) \to (A = [⟨x, y⟩] R \to ψ)$
11	5 8 10	optocl	$⊢ z \in (B \times C) \to (A = [z] R \to ψ)$
12	11	rexlimiv	$⊢ \exists z \in (B \times C) A = [z] R \to ψ$
13	4 12	syl	$⊢ A \in ((B \times C) / R) \to ψ$
14	13 1	eleq2s	$⊢ A \in S \to ψ$

Metamath Proof Explorer