Theorem opth1 5477

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 5470	. . 3 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
4		id 22	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
5	3, 4	eleqtrid 2831	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
6	1	sneqr 4843	. . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
7	6	a1i 11	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} → 𝐴 = 𝐶))
8		oprcl 4901	. . . . . . 7 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simpld 493	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
10		prid1g 4766	. . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷})
11	9, 10	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ {𝐶, 𝐷})
12		eleq2 2814	. . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷}))
13	11, 12	syl5ibrcom 246	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴}))
14		elsni 4647	. . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
15	14	eqcomd 2731	. . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
16	13, 15	syl6 35	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶))
17		id 22	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
18		dfopg 4873	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
19	8, 18	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
20	17, 19	eleqtrd 2827	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}})
21		elpri 4653	. . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
22	20, 21	syl 17	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
23	7, 16, 22	mpjaod 858	. 2 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
24	5, 23	syl 17	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098  Vcvv 3461  {csn 4630  {cpr 4632  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  opth  5478  dmsnopg  6219  funcnvsn  6604  oprabidw  7450  oprabid  7451  seqomlem2  8472  unxpdomlem3  9277  dfac5lem4  10151  dcomex  10472  canthwelem  10675  uzrdgfni  13959  fnpr2ob  17543  gsum2d2  19941  noseqrdgfn  28229  poimirlem9  37230  ichnreuop  46946  ichreuopeq  46947