Metamath Proof Explorer

Theorem optocl

Description: Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995) Shorten and reduce axiom usage. (Revised by TM, 29-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		optocl.1	$⊢ D = B \times C$
2		optocl.2	$⊢ ⟨x, y⟩ = A \to (φ \leftrightarrow ψ)$
3		optocl.3	$⊢ (x \in B \land y \in C) \to φ$
4		elxpi	$⊢ A \in (B \times C) \to \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C))$
5	2	eqcoms	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
6	3 5	imbitrid	$⊢ A = ⟨x, y⟩ \to ((x \in B \land y \in C) \to ψ)$
7	6	imp	$⊢ (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \to ψ$
8	7	exlimivv	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land (x \in B \land y \in C)) \to ψ$
9	4 8	syl	$⊢ A \in (B \times C) \to ψ$
10	9 1	eleq2s	$⊢ A \in D \to ψ$