Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq1 Structured version   Visualization version   GIF version

Theorem opeq1 4433
 Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1
StepHypRef Expression
1 eleq1 2718 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 741 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4220 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4300 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4308 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4142 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4430 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4430 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2710 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  Vcvv 3231  ∅c0 3948  ifcif 4119  {csn 4210  {cpr 4212  ⟨cop 4216 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217 This theorem is referenced by:  opeq12  4435  opeq1i  4436  opeq1d  4439  oteq1  4442  breq1  4688  cbvopab1  4756  cbvopab1s  4758  opthg  4975  eqvinop  4984  opelopabsb  5014  opelxp  5180  elvvv  5212  opabid2  5284  opeliunxp2  5293  elsnres  5471  elimasng  5526  dmsnopg  5642  cnvsngOLD  5659  elsnxpOLD  5716  funopg  5960  f1osng  6215  f1oprswap  6218  dmfco  6311  fvelrn  6392  fsng  6444  fprg  6462  fvrnressn  6468  fvsng  6488  funfvima3  6535  oveq1  6697  oprabid  6717  dfoprab2  6743  cbvoprab1  6769  elxp4  7152  elxp5  7153  opabex3d  7187  opabex3  7188  op1stg  7222  op2ndg  7223  el2xptp  7255  dfoprab4f  7270  frxp  7332  opeliunxp2f  7381  tfrlem11  7529  omeu  7710  oeeui  7727  elixpsn  7989  fundmen  8071  xpsnen  8085  xpassen  8095  xpf1o  8163  unxpdomlem1  8205  dfac5lem1  8984  dfac5lem4  8987  axdc4lem  9315  nqereu  9789  mulcanenq  9820  archnq  9840  prlem934  9893  supsrlem  9970  supsr  9971  swrdccatin1  13529  swrdccat3blem  13541  fsum2dlem  14545  fprod2dlem  14754  vdwlem10  15741  imasaddfnlem  16235  catideu  16383  iscatd2  16389  catlid  16391  catpropd  16416  symg2bas  17864  efgmval  18171  efgi  18178  vrgpval  18226  gsumcom2  18420  txkgen  21503  cnmpt21  21522  xkoinjcn  21538  txconn  21540  pt1hmeo  21657  cnextfvval  21916  qustgplem  21971  dvbsss  23711  axlowdim2  25885  axlowdim  25886  axcontlem10  25898  axcontlem12  25900  isnvlem  27593  br8d  29548  cnvoprabOLD  29626  prsrn  30089  esum2dlem  30282  eulerpartlemgvv  30566  br8  31772  br6  31773  br4  31774  eldm3  31777  br1steqgOLD  31798  br2ndeqgOLD  31799  dfdm5  31800  elfuns  32147  brimg  32169  brapply  32170  brsuccf  32173  brrestrict  32181  dfrdg4  32183  cgrdegen  32236  brofs  32237  cgrextend  32240  brifs  32275  ifscgr  32276  brcgr3  32278  brcolinear2  32290  colineardim1  32293  brfs  32311  idinside  32316  btwnconn1lem7  32325  btwnconn1lem11  32329  btwnconn1lem12  32330  brsegle  32340  outsideofeu  32363  fvray  32373  linedegen  32375  fvline  32376  bj-inftyexpiinv  33225  bj-inftyexpidisj  33227  finxpeq2  33354  finxpreclem6  33363  finxpsuclem  33364  curfv  33519  isdivrngo  33879  drngoi  33880  dicelval3  36786  dihjatcclem4  37027  dropab1  38968  relopabVD  39451
 Copyright terms: Public domain W3C validator