Theorem opeq1 3741

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 2220	. . . . . 6 |- ( A = B -> ( A e. _V <-> B e. _V ) )
2	1	anbi1d 461	. . . . 5 |- ( A = B -> ( ( A e. _V /\ C e. _V ) <-> ( B e. _V /\ C e. _V ) ) )
3		sneq 3571	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3636	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3644	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2227	. . . . 5 |- ( A = B -> ( x e. { { A } , { A , C } } <-> x e. { { B } , { B , C } } ) )
7	2, 6	anbi12d 465	. . . 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 965	. . . 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 965	. . . 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 2275	. 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 3569	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3569	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2215	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963   = wceq 1335   e. wcel 2128   {cab 2143   _Vcvv 2712   {csn 3560   {cpr 3561   <.cop 3563

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 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-sn 3566  df-pr 3567  df-op 3569

This theorem is referenced by:  opeq12  3743  opeq1i  3744  opeq1d  3747  oteq1  3750  breq1  3968  cbvopab1  4037  cbvopab1s  4039  opthg  4197  eqvinop  4202  opelopabsb  4219  opelxp  4613  elvvv  4646  opabid2  4714  opeliunxp2  4723  elsnres  4900  elimasng  4951  rnxpid  5017  dmsnopg  5054  cnvsng  5068  elxp4  5070  elxp5  5071  funopg  5201  f1osng  5452  dmfco  5533  fvelrn  5595  fsng  5637  fvsng  5660  funfvima3  5695  oveq1  5825  oprabid  5847  dfoprab2  5862  cbvoprab1  5887  opabex3d  6063  opabex3  6064  op1stg  6092  op2ndg  6093  oprssdmm  6113  dfoprab4f  6135  cnvoprab  6175  opeliunxp2f  6179  tfr1onlemaccex  6289  tfrcllemaccex  6302  elixpsn  6673  fundmen  6744  xpsnen  6759  xpassen  6768  xpf1o  6782  ltexnqq  7311  archnqq  7320  prarloclemarch2  7322  prarloclemlo  7397  prarloclem3  7400  prarloclem5  7403  caucvgprlemnkj  7569  caucvgprlemnbj  7570  caucvgprlemm  7571  caucvgprlemdisj  7577  caucvgprlemloc  7578  caucvgprlemcl  7579  caucvgprlemladdfu  7580  caucvgprlemladdrl  7581  caucvgprlem1  7582  caucvgprlem2  7583  caucvgpr  7585  caucvgprprlemell  7588  caucvgprprlemelu  7589  caucvgprprlemcbv  7590  caucvgprprlemval  7591  caucvgprprlemnkeqj  7593  caucvgprprlemmu  7598  caucvgprprlemopl  7600  caucvgprprlemlol  7601  caucvgprprlemopu  7602  caucvgprprlemloc  7606  caucvgprprlemclphr  7608  caucvgprprlemexbt  7609  caucvgprprlem1  7612  caucvgprprlem2  7613  caucvgsr  7705  suplocsrlemb  7709  suplocsrlempr  7710  suplocsrlem  7711  suplocsr  7712  elrealeu  7732  pitonn  7751  nntopi  7797  axcaucvglemval  7800  axcaucvg  7803  axpre-suploclemres  7804  fsum2dlemstep  11313  fprod2dlemstep  11501  cnmpt21  12651