This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝐷 = ( 𝐵 × 𝐶 )
		optocl.2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
		optocl.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝜑 )
	Assertion	optoclOLD	⊢ ( 𝐴 ∈ 𝐷 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		optocl.1	⊢ 𝐷 = ( 𝐵 × 𝐶 )
2		optocl.2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		optocl.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) → 𝜑 )
4		elxp3	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )
5		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
6	5 3	sylbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) → 𝜑 )
7	6 2	imbitrid	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) → 𝜓 ) )
8	7	imp	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) → 𝜓 )
9	8	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) → 𝜓 )
10	4 9	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝜓 )
11	10 1	eleq2s	⊢ ( 𝐴 ∈ 𝐷 → 𝜓 )