Metamath Proof Explorer

Theorem optoclOLD

Description: Obsolete version of optocl as of 29-Dec-2025. (Contributed by NM, 5-Mar-1995) (Proof modification is discouraged.) (New usage is discouraged.)

		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	optoclOLD	$⊢ 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		elxp3	$⊢ A \in (B \times C) \leftrightarrow \exists x \exists y (⟨x, y⟩ = A \land ⟨x, y⟩ \in (B \times C))$
5		opelxp	$⊢ ⟨x, y⟩ \in (B \times C) \leftrightarrow (x \in B \land y \in C)$
6	5 3	sylbi	$⊢ ⟨x, y⟩ \in (B \times C) \to φ$
7	6 2	imbitrid	$⊢ ⟨x, y⟩ = A \to (⟨x, y⟩ \in (B \times C) \to ψ)$
8	7	imp	$⊢ (⟨x, y⟩ = A \land ⟨x, y⟩ \in (B \times C)) \to ψ$
9	8	exlimivv	$⊢ \exists x \exists y (⟨x, y⟩ = A \land ⟨x, y⟩ \in (B \times C)) \to ψ$
10	4 9	sylbi	$⊢ A \in (B \times C) \to ψ$
11	10 1	eleq2s	$⊢ A \in D \to ψ$