Metamath Proof Explorer

Theorem 3optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

Ref Expression
Hypotheses 3optocl.1 ⊢ R = D × F
3optocl.2 ⊢ x y = A → φ ↔ ψ
3optocl.3 ⊢ z w = B → ψ ↔ χ
3optocl.4 ⊢ v u = C → χ ↔ θ
3optocl.5 ⊢ x ∈ D ∧ y ∈ F ∧ z ∈ D ∧ w ∈ F ∧ v ∈ D ∧ u ∈ F → φ
Assertion 3optocl ⊢ A ∈ R ∧ B ∈ R ∧ C ∈ R → θ

Proof

Step Hyp Ref Expression
1 3optocl.1 ⊢ R = D × F
2 3optocl.2 ⊢ x y = A → φ ↔ ψ
3 3optocl.3 ⊢ z w = B → ψ ↔ χ
4 3optocl.4 ⊢ v u = C → χ ↔ θ
5 3optocl.5 ⊢ x ∈ D ∧ y ∈ F ∧ z ∈ D ∧ w ∈ F ∧ v ∈ D ∧ u ∈ F → φ
6 4 imbi2d ⊢ v u = C → A ∈ R ∧ B ∈ R → χ ↔ A ∈ R ∧ B ∈ R → θ
7 2 imbi2d ⊢ x y = A → v ∈ D ∧ u ∈ F → φ ↔ v ∈ D ∧ u ∈ F → ψ
8 3 imbi2d ⊢ z w = B → v ∈ D ∧ u ∈ F → ψ ↔ v ∈ D ∧ u ∈ F → χ
9 5 3expia ⊢ x ∈ D ∧ y ∈ F ∧ z ∈ D ∧ w ∈ F → v ∈ D ∧ u ∈ F → φ
10 1 7 8 9 2optocl ⊢ A ∈ R ∧ B ∈ R → v ∈ D ∧ u ∈ F → χ
11 10 com12 ⊢ v ∈ D ∧ u ∈ F → A ∈ R ∧ B ∈ R → χ
12 1 6 11 optocl ⊢ C ∈ R → A ∈ R ∧ B ∈ R → θ
13 12 impcom ⊢ A ∈ R ∧ B ∈ R ∧ C ∈ R → θ
14 13 3impa ⊢ A ∈ R ∧ B ∈ R ∧ C ∈ R → θ