Theorem opeq1 3883

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 2295	. . . . . 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 3700	. . . . . . 7 |- ( A = B -> { A } = { B } )
4		preq1 3768	. . . . . . 7 |- ( A = B -> { A , C } = { B , C } )
5	3, 4	preq12d 3776	. . . . . 6 |- ( A = B -> { { A } , { A , C } } = { { B } , { B , C } } )
6	5	eleq2d 2302	. . . . 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 1007	. . . 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 1007	. . . 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 2352	. 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 3698	. 2 |- <. A , C >. = { x | ( A e. _V /\ C e. _V /\ x e. { { A } , { A , C } } ) }
13		df-op 3698	. 2 |- <. B , C >. = { x | ( B e. _V /\ C e. _V /\ x e. { { B } , { B , C } } ) }
14	11, 12, 13	3eqtr4g 2290	1 |- ( A = B -> <. A , C >. = <. B , C >. )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1005   = wceq 1398   e. wcel 2203   {cab 2218   _Vcvv 2813   {csn 3689   {cpr 3690   <.cop 3692

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698

This theorem is referenced by:  opeq12  3885  opeq1i  3886  opeq1d  3889  oteq1  3892  breq1  4112  cbvopab1  4183  cbvopab1s  4185  opthg  4354  eqvinop  4359  opelopabsb  4378  opelxp  4779  elvvv  4813  opabid2  4886  opeliunxp2  4895  elsnres  5075  elimasng  5130  rnxpid  5197  dmsnopg  5234  cnvsng  5248  elxp4  5250  elxp5  5251  funopg  5386  f1osng  5657  dmfco  5745  fvelrn  5808  fsng  5850  fvsng  5880  funfvima3  5920  oveq1  6057  oprabid  6082  dfoprab2  6100  cbvoprab1  6125  opabex3d  6314  opabex3  6315  op1stg  6344  op2ndg  6345  oprssdmm  6365  dfoprab4f  6387  cnvoprab  6430  opeliunxp2f  6469  tfr1onlemaccex  6579  tfrcllemaccex  6592  elixpsn  6970  fundmen  7047  xpsnen  7072  xpassen  7081  xpf1o  7097  ltexnqq  7723  archnqq  7732  prarloclemarch2  7734  prarloclemlo  7809  prarloclem3  7812  prarloclem5  7815  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemdisj  7989  caucvgprlemloc  7990  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprlem2  7995  caucvgpr  7997  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgsr  8117  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  suplocsr  8124  elrealeu  8144  pitonn  8163  nntopi  8209  axcaucvglemval  8212  axcaucvg  8215  axpre-suploclemres  8216  swrdccatin1  11417  swrdccat3blem  11431  fsum2dlemstep  12120  fprod2dlemstep  12308  imasaddfnlemg  13527  cnmpt21  15156