Theorem opeq1 3833

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 2270	. . . . . 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 3654	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3720	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3728	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2277	. . . . 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 983	. . . 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 983	. . . 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 2325	. 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 3652	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3652	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2265	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981   = wceq 1373   e. wcel 2178   {cab 2193   _Vcvv 2776   {csn 3643   {cpr 3644   <.cop 3646

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652

This theorem is referenced by:  opeq12  3835  opeq1i  3836  opeq1d  3839  oteq1  3842  breq1  4062  cbvopab1  4133  cbvopab1s  4135  opthg  4300  eqvinop  4305  opelopabsb  4324  opelxp  4723  elvvv  4756  opabid2  4827  opeliunxp2  4836  elsnres  5015  elimasng  5069  rnxpid  5136  dmsnopg  5173  cnvsng  5187  elxp4  5189  elxp5  5190  funopg  5324  f1osng  5586  dmfco  5670  fvelrn  5734  fsng  5776  fvsng  5803  funfvima3  5841  oveq1  5974  oprabid  5999  dfoprab2  6015  cbvoprab1  6040  opabex3d  6229  opabex3  6230  op1stg  6259  op2ndg  6260  oprssdmm  6280  dfoprab4f  6302  cnvoprab  6343  opeliunxp2f  6347  tfr1onlemaccex  6457  tfrcllemaccex  6470  elixpsn  6845  fundmen  6922  xpsnen  6941  xpassen  6950  xpf1o  6966  ltexnqq  7556  archnqq  7565  prarloclemarch2  7567  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprlem2  7828  caucvgpr  7830  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgsr  7950  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  suplocsr  7957  elrealeu  7977  pitonn  7996  nntopi  8042  axcaucvglemval  8045  axcaucvg  8048  axpre-suploclemres  8049  swrdccatin1  11216  swrdccat3blem  11230  fsum2dlemstep  11860  fprod2dlemstep  12048  imasaddfnlemg  13261  cnmpt21  14878