Theorem opeq1 3705

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 2202	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 460	. . . . 5 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3538	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3600	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3608	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2209	. . . . 5 |- ( A = B -> ( x e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
7	2, 6	anbi12d 464	. . . 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 964	. . . 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 964	. . . 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 222	. . 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 2257	. 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 3536	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3536	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2197	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 962   = wceq 1331   e. wcel 1480   {cab 2125   _Vcvv 2686   {csn 3527   {cpr 3528   <.cop 3530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536

This theorem is referenced by:  opeq12  3707  opeq1i  3708  opeq1d  3711  oteq1  3714  breq1  3932  cbvopab1  4001  cbvopab1s  4003  opthg  4160  eqvinop  4165  opelopabsb  4182  opelxp  4569  elvvv  4602  opabid2  4670  opeliunxp2  4679  elsnres  4856  elimasng  4907  rnxpid  4973  dmsnopg  5010  cnvsng  5024  elxp4  5026  elxp5  5027  funopg  5157  f1osng  5408  dmfco  5489  fvelrn  5551  fsng  5593  fvsng  5616  funfvima3  5651  oveq1  5781  oprabid  5803  dfoprab2  5818  cbvoprab1  5843  opabex3d  6019  opabex3  6020  op1stg  6048  op2ndg  6049  oprssdmm  6069  dfoprab4f  6091  cnvoprab  6131  opeliunxp2f  6135  tfr1onlemaccex  6245  tfrcllemaccex  6258  elixpsn  6629  fundmen  6700  xpsnen  6715  xpassen  6724  xpf1o  6738  ltexnqq  7216  archnqq  7225  prarloclemarch2  7227  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgprlem2  7488  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkeqj  7498  caucvgprprlemmu  7503  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexbt  7514  caucvgprprlem1  7517  caucvgprprlem2  7518  caucvgsr  7610  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  suplocsr  7617  elrealeu  7637  pitonn  7656  nntopi  7702  axcaucvglemval  7705  axcaucvg  7708  axpre-suploclemres  7709  fsum2dlemstep  11203  cnmpt21  12460