Theorem opeq2 3820

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

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

Proof of Theorem opeq2

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2268	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi2d 464	. . . . 5 |- ( A = B -> ( ( C e. _V /\ A e. _V ) <-> ( C e. _V /\ B e. _V ) ) )
3		eqidd 2206	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3711	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3718	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2275	. . . . 5 |- ( A = B -> ( x e. { { C } , { C , A } } <-> x e. { { C } , { C , B } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) ) )
8		df-3an 983	. . . 4 |- ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( ( C e. _V /\ A e. _V ) /\ x e. { { C } , { C , A } } ) )
9		df-3an 983	. . . 4 |- ( ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) <-> ( ( C e. _V /\ B e. _V ) /\ x e. { { C } , { C , B } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) <-> ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) ) )
11	10	abbidv 2323	. 2 |- ( A = B -> { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) } = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) } )
12		df-op 3642	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3642	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2263	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   = wceq 1373   e. wcel 2176   {cab 2191   _Vcvv 2772   {csn 3633   {cpr 3634   <.cop 3636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642

This theorem is referenced by:  opeq12  3821  opeq2i  3823  opeq2d  3826  oteq2  3829  oteq3  3830  breq2  4049  cbvopab2  4119  cbvopab2v  4122  opthg  4283  eqvinop  4288  opelopabsb  4307  opelxp  4706  opabid2  4810  elrn2g  4869  opeldm  4882  opeldmg  4884  elrn2  4921  opelresg  4967  iss  5006  elimasng  5051  issref  5066  dmsnopg  5155  cnvsng  5169  elxp4  5171  elxp5  5172  dffun5r  5284  funopg  5306  f1osng  5565  tz6.12f  5607  fsn  5754  fsng  5755  fvsng  5782  oveq2  5954  cbvoprab2  6020  ovg  6087  opabex3d  6208  opabex3  6209  op1stg  6238  op2ndg  6239  oprssdmm  6259  op1steq  6267  dfoprab4f  6281  tfrlemibxssdm  6415  tfr1onlembxssdm  6431  tfrcllembxssdm  6444  elixpsn  6824  ixpsnf1o  6825  mapsnen  6905  xpsnen  6918  xpassen  6927  xpf1o  6943  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djulclb  7159  inl11  7169  djuss  7174  1stinl  7178  2ndinl  7179  1stinr  7180  2ndinr  7181  elreal  7943  ax1rid  7992  fseq1p1m1  10218  pfxval  11130  imasaddfnlemg  13179  cnmpt21  14796  djucllem  15773