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

Theorem opeq1 3605
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 2147 . . . . . 6  |-  ( A  =  B  ->  ( A  e.  _V  <->  B  e.  _V ) )
21anbi1d 453 . . . . 5  |-  ( A  =  B  ->  (
( A  e.  _V  /\  C  e.  _V )  <->  ( B  e.  _V  /\  C  e.  _V )
) )
3 sneq 3442 . . . . . . 7  |-  ( A  =  B  ->  { A }  =  { B } )
4 preq1 3502 . . . . . . 7  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
53, 4preq12d 3510 . . . . . 6  |-  ( A  =  B  ->  { { A } ,  { A ,  C } }  =  { { B } ,  { B ,  C } } )
65eleq2d 2154 . . . . 5  |-  ( A  =  B  ->  (
x  e.  { { A } ,  { A ,  C } }  <->  x  e.  { { B } ,  { B ,  C } } ) )
72, 6anbi12d 457 . . . 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 924 . . . 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 924 . . . 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 221 . . 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 2202 . 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 3440 . 2  |-  <. A ,  C >.  =  { x  |  ( A  e. 
_V  /\  C  e.  _V  /\  x  e.  { { A } ,  { A ,  C } } ) }
13 df-op 3440 . 2  |-  <. B ,  C >.  =  { x  |  ( B  e. 
_V  /\  C  e.  _V  /\  x  e.  { { B } ,  { B ,  C } } ) }
1411, 12, 133eqtr4g 2142 1  |-  ( A  =  B  ->  <. A ,  C >.  =  <. B ,  C >. )
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  opeq1i  3608  opeq1d  3611  oteq1  3614  breq1  3823  cbvopab1  3886  cbvopab1s  3888  opthg  4039  eqvinop  4044  opelopabsb  4061  opelxp  4440  elvvv  4469  opabid2  4535  opeliunxp2  4544  elsnres  4716  elimasng  4767  rnxpid  4831  dmsnopg  4868  cnvsng  4882  elxp4  4884  elxp5  4885  funopg  5013  f1osng  5257  dmfco  5335  fvelrn  5393  fsng  5433  fvsng  5456  funfvima3  5489  oveq1  5620  oprabid  5638  dfoprab2  5653  cbvoprab1  5677  opabex3d  5849  opabex3  5850  op1stg  5878  op2ndg  5879  dfoprab4f  5920  cnvoprab  5956  tfr1onlemaccex  6067  tfrcllemaccex  6080  fundmen  6475  xpsnen  6489  xpassen  6498  xpf1o  6512  djur  6701  ltexnqq  6911  archnqq  6920  prarloclemarch2  6922  prarloclemlo  6997  prarloclem3  7000  prarloclem5  7003  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemdisj  7177  caucvgprlemloc  7178  caucvgprlemcl  7179  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  caucvgprlem1  7182  caucvgprlem2  7183  caucvgpr  7185  caucvgprprlemell  7188  caucvgprprlemelu  7189  caucvgprprlemcbv  7190  caucvgprprlemval  7191  caucvgprprlemnkeqj  7193  caucvgprprlemmu  7198  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemopu  7202  caucvgprprlemloc  7206  caucvgprprlemclphr  7208  caucvgprprlemexbt  7209  caucvgprprlem1  7212  caucvgprprlem2  7213  caucvgsr  7291  elrealeu  7311  pitonn  7329  nntopi  7373  axcaucvglemval  7376  axcaucvg  7379
  Copyright terms: Public domain W3C validator