3ecoptocl

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

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

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

Metamath Proof Explorer