Theorem opeq1 3819

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

Assertion

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

Proof of Theorem opeq1

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	anbi1d 465	. . . . 5 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3644	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3710	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3718	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2275	. . . . 5 |- ( A = B -> ( x e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
7	2, 6	anbi12d 473	. . . 4 |- ( A = B -> ( ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) ) )
8		df-3an 983	. . . 4 |- ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( ( A e. _V /\ C e. _V ) /\ x e. { { A } , { A , C } } ) )
9		df-3an 983	. . . 4 |- ( ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) <-> ( ( B e. _V /\ C e. _V ) /\ x e. { { B } , { B , C } } ) )
10	7, 8, 9	3bitr4g 223	. . 3 |- ( A = B -> ( ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) <-> ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) ) )
11	10	abbidv 2323	. 2 |- ( A = B -> { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) } = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) } )
12		df-op 3642	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3642	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2263	1 |- ( A = B -> <. A , C >. = <. B , C >. )

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  opeq1i  3822  opeq1d  3825  oteq1  3828  breq1  4047  cbvopab1  4117  cbvopab1s  4119  opthg  4282  eqvinop  4287  opelopabsb  4306  opelxp  4705  elvvv  4738  opabid2  4809  opeliunxp2  4818  elsnres  4996  elimasng  5050  rnxpid  5117  dmsnopg  5154  cnvsng  5168  elxp4  5170  elxp5  5171  funopg  5305  f1osng  5563  dmfco  5647  fvelrn  5711  fsng  5753  fvsng  5780  funfvima3  5818  oveq1  5951  oprabid  5976  dfoprab2  5992  cbvoprab1  6017  opabex3d  6206  opabex3  6207  op1stg  6236  op2ndg  6237  oprssdmm  6257  dfoprab4f  6279  cnvoprab  6320  opeliunxp2f  6324  tfr1onlemaccex  6434  tfrcllemaccex  6447  elixpsn  6822  fundmen  6898  xpsnen  6916  xpassen  6925  xpf1o  6941  ltexnqq  7521  archnqq  7530  prarloclemarch2  7532  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemdisj  7787  caucvgprlemloc  7788  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprlem2  7793  caucvgpr  7795  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgsr  7915  suplocsrlemb  7919  suplocsrlempr  7920  suplocsrlem  7921  suplocsr  7922  elrealeu  7942  pitonn  7961  nntopi  8007  axcaucvglemval  8010  axcaucvg  8013  axpre-suploclemres  8014  fsum2dlemstep  11745  fprod2dlemstep  11933  imasaddfnlemg  13146  cnmpt21  14763