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  4006  cbvopab1  4076  cbvopab1s  4078  opthg  4238  eqvinop  4243  opelopabsb  4260  opelxp  4656  elvvv  4689  opabid2  4758  opeliunxp2  4767  elsnres  4944  elimasng  4996  rnxpid  5063  dmsnopg  5100  cnvsng  5114  elxp4  5116  elxp5  5117  funopg  5250  f1osng  5502  dmfco  5584  fvelrn  5647  fsng  5689  fvsng  5712  funfvima3  5750  oveq1  5881  oprabid  5906  dfoprab2  5921  cbvoprab1  5946  opabex3d  6121  opabex3  6122  op1stg  6150  op2ndg  6151  oprssdmm  6171  dfoprab4f  6193  cnvoprab  6234  opeliunxp2f  6238  tfr1onlemaccex  6348  tfrcllemaccex  6361  elixpsn  6734  fundmen  6805  xpsnen  6820  xpassen  6829  xpf1o  6843  ltexnqq  7406  archnqq  7415  prarloclemarch2  7417  prarloclemlo  7492  prarloclem3  7495  prarloclem5  7498  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgprlem2  7678  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemelu  7684  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemmu  7693  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexbt  7704  caucvgprprlem1  7707  caucvgprprlem2  7708  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  suplocsr  7807  elrealeu  7827  pitonn  7846  nntopi  7892  axcaucvglemval  7895  axcaucvg  7898  axpre-suploclemres  7899  fsum2dlemstep  11441  fprod2dlemstep  11629  imasaddfnlemg  12734  cnmpt21  13761