2optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

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

Step	Hyp	Ref	Expression
1		2optocl.1	$⊢ R = C \times D$
2		2optocl.2	$⊢ ⟨x, y⟩ = A \to (φ \leftrightarrow ψ)$
3		2optocl.3	$⊢ ⟨z, w⟩ = B \to (ψ \leftrightarrow χ)$
4		2optocl.4	$⊢ ((x \in C \land y \in D) \land (z \in C \land w \in D)) \to φ$
5	3	imbi2d	$⊢ ⟨z, w⟩ = B \to ((A \in R \to ψ) \leftrightarrow (A \in R \to χ))$
6	2	imbi2d	$⊢ ⟨x, y⟩ = 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	optocl	$⊢ A \in R \to ((z \in C \land w \in D) \to ψ)$
9	8	com12	$⊢ (z \in C \land w \in D) \to (A \in R \to ψ)$
10	1 5 9	optocl	$⊢ B \in R \to (A \in R \to χ)$
11	10	impcom	$⊢ (A \in R \land B \in R) \to χ$

Metamath Proof Explorer