Theorem opth1 5421

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 5414	. . 3 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
4		id 22	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
5	3, 4	eleqtrid 2840	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
6	1	sneqr 4794	. . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
7	6	a1i 11	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} → 𝐴 = 𝐶))
8		oprcl 4853	. . . . . . 7 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simpld 494	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
10		prid1g 4715	. . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷})
11	9, 10	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ {𝐶, 𝐷})
12		eleq2 2823	. . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷}))
13	11, 12	syl5ibrcom 247	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴}))
14		elsni 4595	. . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
15	14	eqcomd 2740	. . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
16	13, 15	syl6 35	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶))
17		id 22	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
18		dfopg 4825	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
19	8, 18	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
20	17, 19	eleqtrd 2836	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}})
21		elpri 4602	. . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
22	20, 21	syl 17	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
23	7, 16, 22	mpjaod 860	. 2 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
24	5, 23	syl 17	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578  {cpr 4580  ⟨cop 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585

This theorem is referenced by:  opth  5422  dmsnopg  6169  funcnvsn  6540  oprabidw  7387  oprabid  7388  seqomlem2  8380  unxpdomlem3  9156  dfac5lem4  10034  dfac5lem4OLD  10036  dcomex  10355  canthwelem  10559  uzrdgfni  13879  fnpr2ob  17477  gsum2d2  19901  noseqrdgfn  28267  poimirlem9  37769  ichnreuop  47660  ichreuopeq  47661  diag1f1lem  49493  idfudiag1bas  49711