Theorem opeq2 3806

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 2256	. . . . . 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 2194	. . . . . . 7 |- ( A = B -> { C } = { C } )
4		preq2 3697	. . . . . . 7 |- ( A = B -> { C , A } = { C , B } )
5	3, 4	preq12d 3704	. . . . . 6 |- ( A = B -> { { C } , { C , A } } = { { C } , { C , B } } )
6	5	eleq2d 2263	. . . . 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 982	. . . 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 982	. . . 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 2311	. 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 3628	. 2 |- <. C , A >. = { x | ( C e. _V /\ A e. _V /\ x e. { { C } , { C , A } } ) }
13		df-op 3628	. 2 |- <. C , B >. = { x | ( C e. _V /\ B e. _V /\ x e. { { C } , { C , B } } ) }
14	11, 12, 13	3eqtr4g 2251	1 |- ( A = B -> <. C , A >. = <. C , B >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   = wceq 1364   e. wcel 2164   {cab 2179   _Vcvv 2760   {csn 3619   {cpr 3620   <.cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  opeq12  3807  opeq2i  3809  opeq2d  3812  oteq2  3815  oteq3  3816  breq2  4034  cbvopab2  4104  cbvopab2v  4107  opthg  4268  eqvinop  4273  opelopabsb  4291  opelxp  4690  opabid2  4794  elrn2g  4853  opeldm  4866  opeldmg  4868  elrn2  4905  opelresg  4950  iss  4989  elimasng  5034  issref  5049  dmsnopg  5138  cnvsng  5152  elxp4  5154  elxp5  5155  dffun5r  5267  funopg  5289  f1osng  5542  tz6.12f  5584  fsn  5731  fsng  5732  fvsng  5755  oveq2  5927  cbvoprab2  5992  ovg  6059  opabex3d  6175  opabex3  6176  op1stg  6205  op2ndg  6206  oprssdmm  6226  op1steq  6234  dfoprab4f  6248  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  elixpsn  6791  ixpsnf1o  6792  mapsnen  6867  xpsnen  6877  xpassen  6886  xpf1o  6902  djulclr  7110  djurclr  7111  djulcl  7112  djurcl  7113  djulclb  7116  inl11  7126  djuss  7131  1stinl  7135  2ndinl  7136  1stinr  7137  2ndinr  7138  elreal  7890  ax1rid  7939  fseq1p1m1  10163  imasaddfnlemg  12900  cnmpt21  14470  djucllem  15362