Theorem opth1 5424

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 5417	. . 3 ⊢ {𝐴} ∈ ⟨𝐴, 𝐵⟩
4		id 22	. . 3 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩)
5	3, 4	eleqtrid 2843	. 2 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
6	1	sneqr 4784	. . . 4 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
7	6	a1i 11	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} → 𝐴 = 𝐶))
8		oprcl 4843	. . . . . . 7 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → (𝐶 ∈ V ∧ 𝐷 ∈ V))
9	8	simpld 494	. . . . . 6 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ V)
10		prid1g 4705	. . . . . 6 ⊢ (𝐶 ∈ V → 𝐶 ∈ {𝐶, 𝐷})
11	9, 10	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐶 ∈ {𝐶, 𝐷})
12		eleq2 2826	. . . . 5 ⊢ ({𝐴} = {𝐶, 𝐷} → (𝐶 ∈ {𝐴} ↔ 𝐶 ∈ {𝐶, 𝐷}))
13	11, 12	syl5ibrcom 247	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐶 ∈ {𝐴}))
14		elsni 4585	. . . . 5 ⊢ (𝐶 ∈ {𝐴} → 𝐶 = 𝐴)
15	14	eqcomd 2743	. . . 4 ⊢ (𝐶 ∈ {𝐴} → 𝐴 = 𝐶)
16	13, 15	syl6 35	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶, 𝐷} → 𝐴 = 𝐶))
17		id 22	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ ⟨𝐶, 𝐷⟩)
18		dfopg 4815	. . . . . 6 ⊢ ((𝐶 ∈ V ∧ 𝐷 ∈ V) → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
19	8, 18	syl 17	. . . . 5 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ⟨𝐶, 𝐷⟩ = {{𝐶}, {𝐶, 𝐷}})
20	17, 19	eleqtrd 2839	. . . 4 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → {𝐴} ∈ {{𝐶}, {𝐶, 𝐷}})
21		elpri 4592	. . . 4 ⊢ ({𝐴} ∈ {{𝐶}, {𝐶, 𝐷}} → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
22	20, 21	syl 17	. . 3 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → ({𝐴} = {𝐶} ∨ {𝐴} = {𝐶, 𝐷}))
23	7, 16, 22	mpjaod 861	. 2 ⊢ ({𝐴} ∈ ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)
24	5, 23	syl 17	1 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568  {cpr 4570  ⟨cop 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  opth  5425  dmsnopg  6172  funcnvsn  6543  oprabidw  7392  oprabid  7393  seqomlem2  8384  unxpdomlem3  9162  dfac5lem4  10042  dfac5lem4OLD  10044  dcomex  10363  canthwelem  10567  uzrdgfni  13914  fnpr2ob  17516  gsum2d2  19943  noseqrdgfn  28315  poimirlem9  37967  ichnreuop  47947  ichreuopeq  47948  diag1f1lem  49796  idfudiag1bas  50014