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

Theorem opeq1 3577
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 2116 . . . . . 6  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 446 . . . . 5  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3414 . . . . . . 7  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3475 . . . . . . 7  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3483 . . . . . 6  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
65eleq2d 2123 . . . . 5  |-  ( A  =  B  ->  (
x  e.  { { A } ,  { A ,  C } }  <->  x  e.  { { B } ,  { B ,  C } } ) )
72, 6anbi12d 450 . . . 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 898 . . . 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 898 . . . 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 216 . . 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 2171 . 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 3412 . 2  |-  <. A ,  C >.  =  { x  |  ( A  e. 
_V  /\  C  e.  _V  /\  x  e.  { { A } ,  { A ,  C } } ) }
13 df-op 3412 . 2  |-  <. B ,  C >.  =  { x  |  ( B  e. 
_V  /\  C  e.  _V  /\  x  e.  { { B } ,  { B ,  C } } ) }
1411, 12, 133eqtr4g 2113 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896    = wceq 1259    e. wcel 1409   {cab 2042   _Vcvv 2574   {csn 3403   {cpr 3404   <.cop 3406
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-un 2950  df-sn 3409  df-pr 3410  df-op 3412
This theorem is referenced by:  opeq12  3579  opeq1i  3580  opeq1d  3583  oteq1  3586  breq1  3795  cbvopab1  3858  cbvopab1s  3860  opthg  4003  eqvinop  4008  opelopabsb  4025  opelxp  4402  elvvv  4431  opabid2  4495  opeliunxp2  4504  elsnres  4675  elimasng  4721  rnxpid  4783  dmsnopg  4820  cnvsng  4834  elxp4  4836  elxp5  4837  funopg  4962  f1osng  5195  dmfco  5269  fvelrn  5326  fsng  5364  fvsng  5387  funfvima3  5420  oveq1  5547  oprabid  5565  dfoprab2  5580  cbvoprab1  5604  opabex3d  5776  opabex3  5777  op1stg  5805  op2ndg  5806  dfoprab4f  5847  cnvoprab  5883  fundmen  6317  xpsnen  6326  xpassen  6335  ltexnqq  6564  archnqq  6573  prarloclemarch2  6575  prarloclemlo  6650  prarloclem3  6653  prarloclem5  6656  caucvgprlemnkj  6822  caucvgprlemnbj  6823  caucvgprlemm  6824  caucvgprlemdisj  6830  caucvgprlemloc  6831  caucvgprlemcl  6832  caucvgprlemladdfu  6833  caucvgprlemladdrl  6834  caucvgprlem1  6835  caucvgprlem2  6836  caucvgpr  6838  caucvgprprlemell  6841  caucvgprprlemelu  6842  caucvgprprlemcbv  6843  caucvgprprlemval  6844  caucvgprprlemnkeqj  6846  caucvgprprlemmu  6851  caucvgprprlemopl  6853  caucvgprprlemlol  6854  caucvgprprlemopu  6855  caucvgprprlemloc  6859  caucvgprprlemclphr  6861  caucvgprprlemexbt  6862  caucvgprprlem1  6865  caucvgprprlem2  6866  caucvgsr  6944  elrealeu  6964  pitonn  6982  nntopi  7026  axcaucvglemval  7029  axcaucvg  7032
  Copyright terms: Public domain W3C validator