Theorem opth1 4934

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 4928	. . 3 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
4		id 22	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
5	3, 4	syl5eleq 2705	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
6	1	sneqr 4362	. . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
7	6	a1i 11	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} → 𝐴 = 𝐶))
8		oprcl 4418	. . . . . . 7 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simpld 475	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
10		prid1g 4286	. . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷})
11	9, 10	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ {𝐶, 𝐷})
12		eleq2 2688	. . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷}))
13	11, 12	syl5ibrcom 237	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴}))
14		elsni 4185	. . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
15	14	eqcomd 2626	. . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
16	13, 15	syl6 35	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶))
17		id 22	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
18		dfopg 4391	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
19	8, 18	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
20	17, 19	eleqtrd 2701	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}})
21		elpri 4188	. . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
22	20, 21	syl 17	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
23	7, 16, 22	mpjaod 396	. 2 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
24	5, 23	syl 17	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   = wceq 1481   ∈ wcel 1988  Vcvv 3195  {csn 4168  {cpr 4170  ⟨cop 4174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175

This theorem is referenced by:  opth  4935  dmsnopg  5594  funcnvsn  5924  oprabid  6662  seqomlem2  7531  unxpdomlem3  8151  dfac5lem4  8934  dcomex  9254  canthwelem  9457  uzrdgfni  12740  gsum2d2  18354  poimirlem9  33389