ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq1 Unicode version

Theorem opeq1 3673
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.
StepHypRef Expression
1 eleq1 2178 . . . . . 6  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 458 . . . . 5  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3506 . . . . . . 7  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3568 . . . . . . 7  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3576 . . . . . 6  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
65eleq2d 2185 . . . . 5  |-  ( A  =  B  ->  (
x  e.  { { A } ,  { A ,  C } }  <->  x  e.  { { B } ,  { B ,  C } } ) )
72, 6anbi12d 462 . . . 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 947 . . . 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 947 . . . 4  |-  ( ( B  e.  _V  /\  C  e.  _V  /\  x  e.  { { B } ,  { B ,  C } } )  <->  ( ( B  e.  _V  /\  C  e.  _V )  /\  x  e.  { { B } ,  { B ,  C } } ) )
107, 8, 93bitr4g 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 } } ) ) )
1110abbidv 2233 . 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 3504 . 2  |-  <. A ,  C >.  =  { x  |  ( A  e. 
_V  /\  C  e.  _V  /\  x  e.  { { A } ,  { A ,  C } } ) }
13 df-op 3504 . 2  |-  <. B ,  C >.  =  { x  |  ( B  e. 
_V  /\  C  e.  _V  /\  x  e.  { { B } ,  { B ,  C } } ) }
1411, 12, 133eqtr4g 2173 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945    = wceq 1314    e. wcel 1463   {cab 2101   _Vcvv 2658   {csn 3495   {cpr 3496   <.cop 3498
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-v 2660  df-un 3043  df-sn 3501  df-pr 3502  df-op 3504
This theorem is referenced by:  opeq12  3675  opeq1i  3676  opeq1d  3679  oteq1  3682  breq1  3900  cbvopab1  3969  cbvopab1s  3971  opthg  4128  eqvinop  4133  opelopabsb  4150  opelxp  4537  elvvv  4570  opabid2  4638  opeliunxp2  4647  elsnres  4824  elimasng  4875  rnxpid  4941  dmsnopg  4978  cnvsng  4992  elxp4  4994  elxp5  4995  funopg  5125  f1osng  5374  dmfco  5455  fvelrn  5517  fsng  5559  fvsng  5582  funfvima3  5617  oveq1  5747  oprabid  5769  dfoprab2  5784  cbvoprab1  5809  opabex3d  5985  opabex3  5986  op1stg  6014  op2ndg  6015  oprssdmm  6035  dfoprab4f  6057  cnvoprab  6097  opeliunxp2f  6101  tfr1onlemaccex  6211  tfrcllemaccex  6224  elixpsn  6595  fundmen  6666  xpsnen  6681  xpassen  6690  xpf1o  6704  ltexnqq  7180  archnqq  7189  prarloclemarch2  7191  prarloclemlo  7266  prarloclem3  7269  prarloclem5  7272  caucvgprlemnkj  7438  caucvgprlemnbj  7439  caucvgprlemm  7440  caucvgprlemdisj  7446  caucvgprlemloc  7447  caucvgprlemcl  7448  caucvgprlemladdfu  7449  caucvgprlemladdrl  7450  caucvgprlem1  7451  caucvgprlem2  7452  caucvgpr  7454  caucvgprprlemell  7457  caucvgprprlemelu  7458  caucvgprprlemcbv  7459  caucvgprprlemval  7460  caucvgprprlemnkeqj  7462  caucvgprprlemmu  7467  caucvgprprlemopl  7469  caucvgprprlemlol  7470  caucvgprprlemopu  7471  caucvgprprlemloc  7475  caucvgprprlemclphr  7477  caucvgprprlemexbt  7478  caucvgprprlem1  7481  caucvgprprlem2  7482  caucvgsr  7574  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  suplocsr  7581  elrealeu  7601  pitonn  7620  nntopi  7666  axcaucvglemval  7669  axcaucvg  7672  axpre-suploclemres  7673  fsum2dlemstep  11143  cnmpt21  12355
  Copyright terms: Public domain W3C validator