Theorem opeq1 3777

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  3779  opeq1i  3780  opeq1d  3783  oteq1  3786  breq1  4004  cbvopab1  4074  cbvopab1s  4076  opthg  4236  eqvinop  4241  opelopabsb  4258  opelxp  4654  elvvv  4687  opabid2  4755  opeliunxp2  4764  elsnres  4941  elimasng  4993  rnxpid  5060  dmsnopg  5097  cnvsng  5111  elxp4  5113  elxp5  5114  funopg  5247  f1osng  5499  dmfco  5581  fvelrn  5644  fsng  5686  fvsng  5709  funfvima3  5746  oveq1  5877  oprabid  5902  dfoprab2  5917  cbvoprab1  5942  opabex3d  6117  opabex3  6118  op1stg  6146  op2ndg  6147  oprssdmm  6167  dfoprab4f  6189  cnvoprab  6230  opeliunxp2f  6234  tfr1onlemaccex  6344  tfrcllemaccex  6357  elixpsn  6730  fundmen  6801  xpsnen  6816  xpassen  6825  xpf1o  6839  ltexnqq  7402  archnqq  7411  prarloclemarch2  7413  prarloclemlo  7488  prarloclem3  7491  prarloclem5  7494  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlem1  7673  caucvgprlem2  7674  caucvgpr  7676  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnkeqj  7684  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexbt  7700  caucvgprprlem1  7703  caucvgprprlem2  7704  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  suplocsr  7803  elrealeu  7823  pitonn  7842  nntopi  7888  axcaucvglemval  7891  axcaucvg  7894  axpre-suploclemres  7895  fsum2dlemstep  11433  fprod2dlemstep  11621  cnmpt21  13573