Theorem opth1 5458

Description: Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)

Hypotheses

Ref	Expression
opth1.1	⊢ 𝐴 ∈ V
opth1.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
opth1	⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Proof of Theorem opth1

Step	Hyp	Ref	Expression
1		opth1.1	. . . 4 ⊢ 𝐴 ∈ V
2		opth1.2	. . . 4 ⊢ 𝐵 ∈ V
3	1, 2	opi1 5451	. . 3 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
4		id 23	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
5	3, 4	eleqtrid 2875	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
6	1	sneqr 4809	. . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
7	6	a1i 11	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} → 𝐴 = 𝐶))
8		oprcl 4868	. . . . . . 7 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simpld 499	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
10		prid1g 4731	. . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷})
11	9, 10	syl 18	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ {𝐶, 𝐷})
12		eleq2 2858	. . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷}))
13	11, 12	syl5ibrcom 250	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴}))
14		elsni 4611	. . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
15	14	eqcomd 2775	. . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
16	13, 15	syl6 36	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶))
17		id 23	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
18		dfopg 4840	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
19	8, 18	syl 18	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
20	17, 19	eleqtrd 2871	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}})
21		elpri 4618	. . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
22	20, 21	syl 18	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
23	7, 16, 22	mpjaod 873	. 2 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
24	5, 23	syl 18	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∨ wo 860   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594  {cpr 4596  ⟨cop 4600

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601

This theorem is referenced by:  opth  5459  dmsnopg  6215  funcnvsn  6587  oprabidw  7442  oprabid  7443  seqomlem2  8438  unxpdomlem3  9218  dfac5lem4  10110  dcomex  10431  canthwelem  10635  uzrdgfni  13994  fnpr2ob  17612  gsum2d2  20044  noseqrdgfn  28465  poimirlem9  38168  ichnreuop  48110  ichreuopeq  48111  diag1f1lem  49969  idfudiag1bas  50187