Theorem 3ecoptocl

Description: Implicit substitution of classes for equivalence classes of ordered pairs. (Contributed by NM, 9-Aug-1995)

	Ref	Expression
Hypotheses	3ecoptocl.1	⊢ 𝑆 = ( ( 𝐷 × 𝐷 ) / 𝑅 )
	3ecoptocl.2	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	3ecoptocl.3	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] 𝑅 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	3ecoptocl.4	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] 𝑅 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
	3ecoptocl.5	⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜑 )
Assertion	3ecoptocl	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		3ecoptocl.1	⊢ 𝑆 = ( ( 𝐷 × 𝐷 ) / 𝑅 )
2		3ecoptocl.2	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		3ecoptocl.3	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] 𝑅 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
4		3ecoptocl.4	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] 𝑅 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
5		3ecoptocl.5	⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜑 )
6	3	imbi2d	⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] 𝑅 = 𝐵 → ( ( 𝐴 ∈ 𝑆 → 𝜓 ) ↔ ( 𝐴 ∈ 𝑆 → 𝜒 ) ) )
7	4	imbi2d	⊢ ( [ ⟨ 𝑣 , 𝑢 ⟩ ] 𝑅 = 𝐶 → ( ( 𝐴 ∈ 𝑆 → 𝜒 ) ↔ ( 𝐴 ∈ 𝑆 → 𝜃 ) ) )
8	2	imbi2d	⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] 𝑅 = 𝐴 → ( ( ( ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜑 ) ↔ ( ( ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜓 ) ) )
9	5	3expib	⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜑 ) )
10	1 8 9	ecoptocl	⊢ ( 𝐴 ∈ 𝑆 → ( ( ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → 𝜓 ) )
11	10	com12	⊢ ( ( ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐷 ) ) → ( 𝐴 ∈ 𝑆 → 𝜓 ) )
12	1 6 7 11	2ecoptocl	⊢ ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → ( 𝐴 ∈ 𝑆 → 𝜃 ) )
13	12	com12	⊢ ( 𝐴 ∈ 𝑆 → ( ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝜃 ) )
14	13	3impib	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆 ) → 𝜃 )