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

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

Proof

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