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

Theorem opeq1 4375
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 2692 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 740 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4163 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4243 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4251 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4086 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4372 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4372 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2685 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1480  wcel 1992  Vcvv 3191  c0 3896  ifcif 4063  {csn 4153  {cpr 4155  cop 4159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160
This theorem is referenced by:  opeq12  4377  opeq1i  4378  opeq1d  4381  oteq1  4384  breq1  4621  cbvopab1  4690  cbvopab1s  4692  opthg  4911  eqvinop  4920  opelopabsb  4950  opelxp  5111  elvvv  5144  opabid2  5216  opeliunxp2  5225  elsnres  5399  elimasng  5454  dmsnopg  5568  cnvsng  5583  elsnxpOLD  5640  funopg  5882  f1osng  6136  f1oprswap  6139  dmfco  6230  fvelrn  6309  fsng  6359  fprg  6377  fvrnressn  6383  fvsng  6402  funfvima3  6450  oveq1  6612  oprabid  6632  dfoprab2  6655  cbvoprab1  6681  elxp4  7060  elxp5  7061  opabex3d  7094  opabex3  7095  op1stg  7128  op2ndg  7129  el2xptp  7159  dfoprab4f  7174  frxp  7233  opeliunxp2f  7282  tfrlem11  7430  omeu  7611  oeeui  7628  elixpsn  7892  fundmen  7975  xpsnen  7989  xpassen  7999  xpf1o  8067  unxpdomlem1  8109  dfac5lem1  8891  dfac5lem4  8894  axdc4lem  9222  nqereu  9696  mulcanenq  9727  archnq  9747  prlem934  9800  supsrlem  9877  supsr  9878  swrdccatin1  13415  swrdccat3blem  13427  fsum2dlem  14424  fprod2dlem  14630  vdwlem10  15613  imasaddfnlem  16104  catideu  16252  iscatd2  16258  catlid  16260  catpropd  16285  symg2bas  17734  efgmval  18041  efgi  18048  vrgpval  18096  gsumcom2  18290  txkgen  21360  cnmpt21  21379  xkoinjcn  21395  txconn  21397  pt1hmeo  21514  cnextfvval  21774  qustgplem  21829  dvbsss  23567  axlowdim2  25735  axlowdim  25736  axcontlem10  25748  axcontlem12  25750  isnvlem  27305  br8d  29256  cnvoprab  29332  prsrn  29735  esum2dlem  29927  eulerpartlemgvv  30211  br8  31345  br6  31346  br4  31347  eldm3  31351  br1steqg  31364  br2ndeqg  31365  dfdm5  31366  elfuns  31637  brimg  31659  brapply  31660  brsuccf  31663  brrestrict  31671  dfrdg4  31673  cgrdegen  31726  brofs  31727  cgrextend  31730  brifs  31765  ifscgr  31766  brcgr3  31768  brcolinear2  31780  colineardim1  31783  brfs  31801  idinside  31806  btwnconn1lem7  31815  btwnconn1lem11  31819  btwnconn1lem12  31820  brsegle  31830  outsideofeu  31853  fvray  31863  linedegen  31865  fvline  31866  bj-inftyexpiinv  32701  bj-inftyexpidisj  32703  finxpeq2  32829  finxpreclem6  32838  finxpsuclem  32839  curfv  32988  isdivrngo  33348  drngoi  33349  dicelval3  35916  dihjatcclem4  36157  dropab1  38100  relopabVD  38587
  Copyright terms: Public domain W3C validator