![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3optocl | Structured version Visualization version GIF version |
Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995.) |
Ref | Expression |
---|---|
3optocl.1 | ⊢ 𝑅 = (𝐷 × 𝐹) |
3optocl.2 | ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (𝜑 ↔ 𝜓)) |
3optocl.3 | ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (𝜓 ↔ 𝜒)) |
3optocl.4 | ⊢ (〈𝑣, 𝑢〉 = 𝐶 → (𝜒 ↔ 𝜃)) |
3optocl.5 | ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹)) → 𝜑) |
Ref | Expression |
---|---|
3optocl | ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3optocl.1 | . . . 4 ⊢ 𝑅 = (𝐷 × 𝐹) | |
2 | 3optocl.4 | . . . . 5 ⊢ (〈𝑣, 𝑢〉 = 𝐶 → (𝜒 ↔ 𝜃)) | |
3 | 2 | imbi2d 340 | . . . 4 ⊢ (〈𝑣, 𝑢〉 = 𝐶 → (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜒) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜃))) |
4 | 3optocl.2 | . . . . . . 7 ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 4 | imbi2d 340 | . . . . . 6 ⊢ (〈𝑥, 𝑦〉 = 𝐴 → (((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜑) ↔ ((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜓))) |
6 | 3optocl.3 | . . . . . . 7 ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (𝜓 ↔ 𝜒)) | |
7 | 6 | imbi2d 340 | . . . . . 6 ⊢ (〈𝑧, 𝑤〉 = 𝐵 → (((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜓) ↔ ((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜒))) |
8 | 3optocl.5 | . . . . . . 7 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹) ∧ (𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹)) → 𝜑) | |
9 | 8 | 3expia 1121 | . . . . . 6 ⊢ (((𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹) ∧ (𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹)) → ((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜑)) |
10 | 1, 5, 7, 9 | 2optocl 5769 | . . . . 5 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → ((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → 𝜒)) |
11 | 10 | com12 32 | . . . 4 ⊢ ((𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹) → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜒)) |
12 | 1, 3, 11 | optocl 5768 | . . 3 ⊢ (𝐶 ∈ 𝑅 → ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) → 𝜃)) |
13 | 12 | impcom 408 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅) ∧ 𝐶 ∈ 𝑅) → 𝜃) |
14 | 13 | 3impa 1110 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 〈cop 4633 × cxp 5673 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-opab 5210 df-xp 5681 |
This theorem is referenced by: ecopovtrn 8810 |
Copyright terms: Public domain | W3C validator |