Theorem opeq1 3805

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 2256	. . . . . 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 3630	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3696	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3704	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2263	. . . . 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 982	. . . 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 982	. . . 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 2311	. 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 3628	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3628	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2251	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 980   = wceq 1364   e. wcel 2164   {cab 2179   _Vcvv 2760   {csn 3619   {cpr 3620   <.cop 3622

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-un 3158  df-sn 3625  df-pr 3626  df-op 3628

This theorem is referenced by:  opeq12  3807  opeq1i  3808  opeq1d  3811  oteq1  3814  breq1  4033  cbvopab1  4103  cbvopab1s  4105  opthg  4268  eqvinop  4273  opelopabsb  4291  opelxp  4690  elvvv  4723  opabid2  4794  opeliunxp2  4803  elsnres  4980  elimasng  5034  rnxpid  5101  dmsnopg  5138  cnvsng  5152  elxp4  5154  elxp5  5155  funopg  5289  f1osng  5542  dmfco  5626  fvelrn  5690  fsng  5732  fvsng  5755  funfvima3  5793  oveq1  5926  oprabid  5951  dfoprab2  5966  cbvoprab1  5991  opabex3d  6175  opabex3  6176  op1stg  6205  op2ndg  6206  oprssdmm  6226  dfoprab4f  6248  cnvoprab  6289  opeliunxp2f  6293  tfr1onlemaccex  6403  tfrcllemaccex  6416  elixpsn  6791  fundmen  6862  xpsnen  6877  xpassen  6886  xpf1o  6902  ltexnqq  7470  archnqq  7479  prarloclemarch2  7481  prarloclemlo  7556  prarloclem3  7559  prarloclem5  7562  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemdisj  7736  caucvgprlemloc  7737  caucvgprlemcl  7738  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgpr  7744  caucvgprprlemell  7747  caucvgprprlemelu  7748  caucvgprprlemcbv  7749  caucvgprprlemval  7750  caucvgprprlemnkeqj  7752  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemopu  7761  caucvgprprlemloc  7765  caucvgprprlemclphr  7767  caucvgprprlemexbt  7768  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgsr  7864  suplocsrlemb  7868  suplocsrlempr  7869  suplocsrlem  7870  suplocsr  7871  elrealeu  7891  pitonn  7910  nntopi  7956  axcaucvglemval  7959  axcaucvg  7962  axpre-suploclemres  7963  fsum2dlemstep  11580  fprod2dlemstep  11768  imasaddfnlemg  12900  cnmpt21  14470