Theorem opeq1 3778

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

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

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601

This theorem is referenced by:  opeq12  3780  opeq1i  3781  opeq1d  3784  oteq1  3787  breq1  4005  cbvopab1  4075  cbvopab1s  4077  opthg  4237  eqvinop  4242  opelopabsb  4259  opelxp  4655  elvvv  4688  opabid2  4757  opeliunxp2  4766  elsnres  4943  elimasng  4995  rnxpid  5062  dmsnopg  5099  cnvsng  5113  elxp4  5115  elxp5  5116  funopg  5249  f1osng  5501  dmfco  5583  fvelrn  5646  fsng  5688  fvsng  5711  funfvima3  5748  oveq1  5879  oprabid  5904  dfoprab2  5919  cbvoprab1  5944  opabex3d  6119  opabex3  6120  op1stg  6148  op2ndg  6149  oprssdmm  6169  dfoprab4f  6191  cnvoprab  6232  opeliunxp2f  6236  tfr1onlemaccex  6346  tfrcllemaccex  6359  elixpsn  6732  fundmen  6803  xpsnen  6818  xpassen  6827  xpf1o  6841  ltexnqq  7404  archnqq  7413  prarloclemarch2  7415  prarloclemlo  7490  prarloclem3  7493  prarloclem5  7496  caucvgprlemnkj  7662  caucvgprlemnbj  7663  caucvgprlemm  7664  caucvgprlemdisj  7670  caucvgprlemloc  7671  caucvgprlemcl  7672  caucvgprlemladdfu  7673  caucvgprlemladdrl  7674  caucvgprlem1  7675  caucvgprlem2  7676  caucvgpr  7678  caucvgprprlemell  7681  caucvgprprlemelu  7682  caucvgprprlemcbv  7683  caucvgprprlemval  7684  caucvgprprlemnkeqj  7686  caucvgprprlemmu  7691  caucvgprprlemopl  7693  caucvgprprlemlol  7694  caucvgprprlemopu  7695  caucvgprprlemloc  7699  caucvgprprlemclphr  7701  caucvgprprlemexbt  7702  caucvgprprlem1  7705  caucvgprprlem2  7706  caucvgsr  7798  suplocsrlemb  7802  suplocsrlempr  7803  suplocsrlem  7804  suplocsr  7805  elrealeu  7825  pitonn  7844  nntopi  7890  axcaucvglemval  7893  axcaucvg  7896  axpre-suploclemres  7897  fsum2dlemstep  11435  fprod2dlemstep  11623  cnmpt21  13662