2ecoptocl

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

	Ref	Expression
Hypotheses	2ecoptocl.1	$⊢ S = (C \times D) / R$
	2ecoptocl.2	$⊢ [⟨x, y⟩] R = A \to (φ \leftrightarrow ψ)$
	2ecoptocl.3	$⊢ [⟨z, w⟩] R = B \to (ψ \leftrightarrow χ)$
	2ecoptocl.4	$⊢ ((x \in C \land y \in D) \land (z \in C \land w \in D)) \to φ$
Assertion	2ecoptocl	$⊢ (A \in S \land B \in S) \to χ$

Step	Hyp	Ref	Expression
1		2ecoptocl.1	$⊢ S = (C \times D) / R$
2		2ecoptocl.2	$⊢ [⟨x, y⟩] R = A \to (φ \leftrightarrow ψ)$
3		2ecoptocl.3	$⊢ [⟨z, w⟩] R = B \to (ψ \leftrightarrow χ)$
4		2ecoptocl.4	$⊢ ((x \in C \land y \in D) \land (z \in C \land w \in D)) \to φ$
5	3	imbi2d	$⊢ [⟨z, w⟩] R = B \to ((A \in S \to ψ) \leftrightarrow (A \in S \to χ))$
6	2	imbi2d	$⊢ [⟨x, y⟩] R = A \to (((z \in C \land w \in D) \to φ) \leftrightarrow ((z \in C \land w \in D) \to ψ))$
7	4	ex	$⊢ (x \in C \land y \in D) \to ((z \in C \land w \in D) \to φ)$
8	1 6 7	ecoptocl	$⊢ A \in S \to ((z \in C \land w \in D) \to ψ)$
9	8	com12	$⊢ (z \in C \land w \in D) \to (A \in S \to ψ)$
10	1 5 9	ecoptocl	$⊢ B \in S \to (A \in S \to χ)$
11	10	impcom	$⊢ (A \in S \land B \in S) \to χ$

Metamath Proof Explorer