![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opthg | Structured version Visualization version GIF version |
Description: Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opthg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1 4678 | . . . 4 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
2 | 1 | eqeq1d 2780 | . . 3 ⊢ (𝑥 = 𝐴 → (〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉)) |
3 | eqeq1 2782 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
4 | 3 | anbi1d 620 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷))) |
5 | 2, 4 | bibi12d 338 | . 2 ⊢ (𝑥 = 𝐴 → ((〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)))) |
6 | opeq2 4679 | . . . 4 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
7 | 6 | eqeq1d 2780 | . . 3 ⊢ (𝑦 = 𝐵 → (〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉)) |
8 | eqeq1 2782 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷)) | |
9 | 8 | anbi2d 619 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
10 | 7, 9 | bibi12d 338 | . 2 ⊢ (𝑦 = 𝐵 → ((〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))) |
11 | vex 3418 | . . 3 ⊢ 𝑥 ∈ V | |
12 | vex 3418 | . . 3 ⊢ 𝑦 ∈ V | |
13 | 11, 12 | opth 5226 | . 2 ⊢ (〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) |
14 | 5, 10, 13 | vtocl2g 3490 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 〈cop 4448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 |
This theorem is referenced by: opth1g 5228 opthg2 5229 opthneg 5231 otthg 5235 oteqex 5247 s111 13781 embedsetcestrclem 17268 symg2bas 18290 frgpnabllem1 18752 frgpnabllem2 18753 mat1dimbas 20788 linds2eq 30612 opideq 35046 dvheveccl 37693 hoidmv1le 42308 oppr 42671 opprb 42672 prproropf1olem4 43037 |
Copyright terms: Public domain | W3C validator |