Theorem opeq2 3780

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 2240	. . . . . 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 2178	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3671	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3678	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2247	. . . . 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 980	. . . 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 980	. . . 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 2295	. 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 3602	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3602	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2235	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 978   = wceq 1353   e. wcel 2148   {cab 2163   _Vcvv 2738   {csn 3593   {cpr 3594   <.cop 3596

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602

This theorem is referenced by:  opeq12  3781  opeq2i  3783  opeq2d  3786  oteq2  3789  oteq3  3790  breq2  4008  cbvopab2  4078  cbvopab2v  4081  opthg  4239  eqvinop  4244  opelopabsb  4261  opelxp  4657  opabid2  4759  elrn2g  4818  opeldm  4831  opeldmg  4833  elrn2  4870  opelresg  4915  iss  4954  elimasng  4997  issref  5012  dmsnopg  5101  cnvsng  5115  elxp4  5117  elxp5  5118  dffun5r  5229  funopg  5251  f1osng  5503  tz6.12f  5545  fsn  5689  fsng  5690  fvsng  5713  oveq2  5883  cbvoprab2  5948  ovg  6013  opabex3d  6122  opabex3  6123  op1stg  6151  op2ndg  6152  oprssdmm  6172  op1steq  6180  dfoprab4f  6194  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  elixpsn  6735  ixpsnf1o  6736  mapsnen  6811  xpsnen  6821  xpassen  6830  xpf1o  6844  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djulclb  7054  inl11  7064  djuss  7069  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  elreal  7827  ax1rid  7876  fseq1p1m1  10094  imasaddfnlemg  12735  cnmpt21  13794  djucllem  14555