|   | 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 4872 | . . . 4 ⊢ (𝑥 = 𝐴 → 〈𝑥, 𝑦〉 = 〈𝐴, 𝑦〉) | |
| 2 | 1 | eqeq1d 2738 | . . 3 ⊢ (𝑥 = 𝐴 → (〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉)) | 
| 3 | eqeq1 2740 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 = 𝐶 ↔ 𝐴 = 𝐶)) | |
| 4 | 3 | anbi1d 631 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷))) | 
| 5 | 2, 4 | bibi12d 345 | . 2 ⊢ (𝑥 = 𝐴 → ((〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)))) | 
| 6 | opeq2 4873 | . . . 4 ⊢ (𝑦 = 𝐵 → 〈𝐴, 𝑦〉 = 〈𝐴, 𝐵〉) | |
| 7 | 6 | eqeq1d 2738 | . . 3 ⊢ (𝑦 = 𝐵 → (〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ 〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉)) | 
| 8 | eqeq1 2740 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝑦 = 𝐷 ↔ 𝐵 = 𝐷)) | |
| 9 | 8 | anbi2d 630 | . . 3 ⊢ (𝑦 = 𝐵 → ((𝐴 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | 
| 10 | 7, 9 | bibi12d 345 | . 2 ⊢ (𝑦 = 𝐵 → ((〈𝐴, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))) | 
| 11 | vex 3483 | . . 3 ⊢ 𝑥 ∈ V | |
| 12 | vex 3483 | . . 3 ⊢ 𝑦 ∈ V | |
| 13 | 11, 12 | opth 5480 | . 2 ⊢ (〈𝑥, 𝑦〉 = 〈𝐶, 𝐷〉 ↔ (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) | 
| 14 | 5, 10, 13 | vtocl2g 3573 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 = 〈𝐶, 𝐷〉 ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 〈cop 4631 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 | 
| This theorem is referenced by: opth1g 5482 opthg2 5483 opthneg 5485 otthg 5489 oteqex 5504 s111 14654 embedsetcestrclem 18203 symg2bas 19411 frgpnabllem1 19892 frgpnabllem2 19893 mat1dimbas 22479 linds2eq 33410 goeleq12bg 35355 opideq 38345 dvheveccl 41115 hoidmv1le 46614 oppr 47047 opprb 47048 fsetsnf1 47069 prproropf1olem4 47498 fuco2 49041 | 
| Copyright terms: Public domain | W3C validator |