Theorem opth2 3546

Description: Equality of the second members of equal ordered pairs. Because of our particular ordered pair definition, equality holds whether or not the first members are sets.

Hypotheses

Ref	Expression
opth2.1	|- B e. _V
opth2.2	|- D e. _V

Assertion

Ref	Expression
opth2	|- (<.A, B>. = <.C, D>. -> B = D)

Proof of Theorem opth2

Step	Hyp	Ref	Expression
1		opeq1 3158	. . . . 5 |- (x = A -> <.x, B>. = <.A, B>.)
2	1	eqeq1d 1892	. . . 4 |- (x = A -> (<.x, B>. = <.C, D>. <-> <.A, B>. = <.C, D>.))
3	2	imbi1d 675	. . 3 |- (x = A -> ((<.x, B>. = <.C, D>. -> B = D) <-> (<.A, B>. = <.C, D>. -> B = D)))
4		visset 2295	. . . . 5 |- x e. _V
5		opth2.1	. . . . 5 |- B e. _V
6		opth2.2	. . . . 5 |- D e. _V
7	4, 5, 6	opth 3532	. . . 4 |- (<.x, B>. = <.C, D>. <-> (x = C /\ B = D))
8	7	simprbi 353	. . 3 |- (<.x, B>. = <.C, D>. -> B = D)
9	3, 8	vtoclg 2346	. 2 |- (A e. _V -> (<.A, B>. = <.C, D>. -> B = D))
10		nelneq2 1986	. . . . 5 |- (((/) e. <.A, B>. /\ -. (/) e. <.C, D>.) -> -. <.A, B>. = <.C, D>.)
11		opprc1b 3542	. . . . 5 |- (-. A e. _V <-> (/) e. <.A, B>.)
12		opprc1b 3542	. . . . . . 7 |- (-. C e. _V <-> (/) e. <.C, D>.)
13	12	con1bii 237	. . . . . 6 |- (-. (/) e. <.C, D>. <-> C e. _V)
14	13	bicomi 189	. . . . 5 |- (C e. _V <-> -. (/) e. <.C, D>.)
15	10, 11, 14	syl2anb 504	. . . 4 |- ((-. A e. _V /\ C e. _V) -> -. <.A, B>. = <.C, D>.)
16	15	pm2.21d 94	. . 3 |- ((-. A e. _V /\ C e. _V) -> (<.A, B>. = <.C, D>. -> B = D))
17		opprc1 3170	. . . . 5 |- (-. A e. _V -> <.A, B>. = {(/), {B}})
18		opprc1 3170	. . . . 5 |- (-. C e. _V -> <.C, D>. = {(/), {D}})
19	17, 18	eqeqan12d 1901	. . . 4 |- ((-. A e. _V /\ -. C e. _V) -> (<.A, B>. = <.C, D>. <-> {(/), {B}} = {(/), {D}}))
20		snex 3492	. . . . . 6 |- {B} e. _V
21		snex 3492	. . . . . 6 |- {D} e. _V
22	20, 21	preqr2 3153	. . . . 5 |- ({(/), {B}} = {(/), {D}} -> {B} = {D})
23	5	sneqr 3147	. . . . 5 |- ({B} = {D} -> B = D)
24	22, 23	syl 12	. . . 4 |- ({(/), {B}} = {(/), {D}} -> B = D)
25	19, 24	syl6bi 231	. . 3 |- ((-. A e. _V /\ -. C e. _V) -> (<.A, B>. = <.C, D>. -> B = D))
26	16, 25	pm2.61dan 535	. 2 |- (-. A e. _V -> (<.A, B>. = <.C, D>. -> B = D))
27	9, 26	pm2.61i 140	1 |- (<.A, B>. = <.C, D>. -> B = D)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  _Vcvv 2292  (/)c0 2875  {csn 3044  {cpr 3045  <.cop 3046

This theorem is referenced by:  moop2 3548  funsnOLD 4464  cbcpcp 14504  filnetlem4 15643  filnetlem5 15644  filnet 15645  prfunOLD 15677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053

Copyright terms: Public domain