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

Theorem opeq2 3606
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq2  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )

Proof of Theorem opeq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 eleq1 2147 . . . . . 6  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi2d 452 . . . . 5  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V )  <->  ( C  e.  _V  /\  B  e.  _V )
) )
3 eqidd 2086 . . . . . . 7  |-  ( A  =  B  ->  { C }  =  { C } )
4 preq2 3503 . . . . . . 7  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
53, 4preq12d 3510 . . . . . 6  |-  ( A  =  B  ->  { { C } ,  { C ,  A } }  =  { { C } ,  { C ,  B } } )
65eleq2d 2154 . . . . 5  |-  ( A  =  B  ->  (
x  e.  { { C } ,  { C ,  A } }  <->  x  e.  { { C } ,  { C ,  B } } ) )
72, 6anbi12d 457 . . . 4  |-  ( A  =  B  ->  (
( ( C  e. 
_V  /\  A  e.  _V )  /\  x  e.  { { C } ,  { C ,  A } } )  <->  ( ( C  e.  _V  /\  B  e.  _V )  /\  x  e.  { { C } ,  { C ,  B } } ) ) )
8 df-3an 924 . . . 4  |-  ( ( C  e.  _V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } )  <->  ( ( C  e.  _V  /\  A  e.  _V )  /\  x  e.  { { C } ,  { C ,  A } } ) )
9 df-3an 924 . . . 4  |-  ( ( C  e.  _V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } )  <->  ( ( C  e.  _V  /\  B  e.  _V )  /\  x  e.  { { C } ,  { C ,  B } } ) )
107, 8, 93bitr4g 221 . . 3  |-  ( A  =  B  ->  (
( C  e.  _V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } )  <-> 
( C  e.  _V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } ) ) )
1110abbidv 2202 . 2  |-  ( A  =  B  ->  { x  |  ( C  e. 
_V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } ) }  =  { x  |  ( C  e.  _V  /\  B  e.  _V  /\  x  e. 
{ { C } ,  { C ,  B } } ) } )
12 df-op 3440 . 2  |-  <. C ,  A >.  =  { x  |  ( C  e. 
_V  /\  A  e.  _V  /\  x  e.  { { C } ,  { C ,  A } } ) }
13 df-op 3440 . 2  |-  <. C ,  B >.  =  { x  |  ( C  e. 
_V  /\  B  e.  _V  /\  x  e.  { { C } ,  { C ,  B } } ) }
1411, 12, 133eqtr4g 2142 1  |-  ( A  =  B  ->  <. C ,  A >.  =  <. C ,  B >. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 922    = wceq 1287    e. wcel 1436   {cab 2071   _Vcvv 2615   {csn 3431   {cpr 3432   <.cop 3434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440
This theorem is referenced by:  opeq12  3607  opeq2i  3609  opeq2d  3612  oteq2  3615  oteq3  3616  breq2  3824  cbvopab2  3887  cbvopab2v  3890  opthg  4039  eqvinop  4044  opelopabsb  4061  opelxp  4440  opabid2  4535  elrn2g  4594  opeldm  4607  opeldmg  4609  elrn2  4645  opelresg  4688  iss  4725  elimasng  4767  issref  4781  dmsnopg  4868  cnvsng  4882  elxp4  4884  elxp5  4885  dffun5r  4993  funopg  5013  f1osng  5257  tz6.12f  5296  fsn  5432  fsng  5433  fvsng  5456  oveq2  5621  cbvoprab2  5678  ovg  5740  opabex3d  5849  opabex3  5850  op1stg  5878  op2ndg  5879  op1steq  5906  dfoprab4f  5920  tfrlemibxssdm  6046  tfr1onlembxssdm  6062  tfrcllembxssdm  6075  mapsnen  6480  xpsnen  6489  xpassen  6498  xpf1o  6512  djulclr  6685  djurclr  6686  djulcl  6687  djurcl  6688  djulclb  6691  djur  6701  djuss  6705  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  elreal  7310  ax1rid  7356  fseq1p1m1  9438  djucllem  11145
  Copyright terms: Public domain W3C validator