Theorem optocl

Description: Implicit substitution of class for ordered pair. (Contributed by NM, 5-Mar-1995)

	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		elxp3	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )
5		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) )
6	5 3	sylbi	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) → 𝜑 )
7	6 2	syl5ib	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) → 𝜓 ) )
8	7	imp	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) → 𝜓 )
9	8	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐵 × 𝐶 ) ) → 𝜓 )
10	4 9	sylbi	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) → 𝜓 )
11	10 1	eleq2s	⊢ ( 𝐴 ∈ 𝐷 → 𝜓 )