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

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

Proof of Theorem opeq2
StepHypRef Expression
1 eleq1 2898 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 630 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 preq2 4662 . . . 4 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
43preq2d 4668 . . 3 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
52, 4ifbieq1d 4488 . 2 (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6 dfopif 4792 . 2 𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7 dfopif 4792 . 2 𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
85, 6, 73eqtr4g 2879 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   = wceq 1530   ∈ wcel 2107  Vcvv 3493  ∅c0 4289  ifcif 4465  {csn 4559  {cpr 4561  ⟨cop 4565 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566 This theorem is referenced by:  opeq12  4797  opeq2i  4799  opeq2d  4802  oteq2  4805  oteq3  4806  breq2  5061  cbvopab2  5132  cbvopab2v  5135  opthg  5360  eqvinop  5369  opelopabsb  5408  dfid3  5455  opelxp  5584  relopabi  5687  opabid2  5693  elrn2g  5754  opeldmd  5768  opeldm  5769  elrn2  5814  iss  5896  elidinxp  5904  elimasng  5948  dmsnopg  6063  reuop  6137  funopg  6382  f1osng  6648  f1oprswap  6651  tz6.12f  6687  fvn0ssdmfun  6835  fsn  6890  fsng  6892  fprg  6910  fprb  6949  oveq2  7156  cbvoprab2  7234  ovg  7305  elxp4  7619  elxp5  7620  opabex3d  7658  opabex3rd  7659  opabex3  7660  op1stg  7693  op2ndg  7694  op1steq  7725  dfoprab4f  7746  fsplit  7804  seqomlem2  8079  omeu  8203  oeeui  8220  ralxpmap  8452  elixpsn  8493  ixpsnf1o  8494  mapsnend  8580  xpsnen  8593  xpassen  8603  xpf1o  8671  unxpdomlem1  8714  djulcl  9331  djurcl  9332  djur  9340  djuss  9341  djuun  9347  1stinl  9348  2ndinl  9349  1stinr  9350  2ndinr  9351  axdc4lem  9869  nqereu  10343  mulcanenq  10374  elreal  10545  ax1rid  10575  fseq1p1m1  12973  pfxval  14027  swrdccatin1  14079  swrdccat3blem  14093  wrdlen2  14298  ruclem1  15576  imasaddfnlem  16793  imasvscafn  16802  catidex  16937  catpropd  16971  funcsetcestrclem1  17396  symg2bas  18513  efgi  18837  gsumcom2  19087  mat1rhmval  21080  mat1ric  21088  txkgen  22252  cnmpt21  22271  xkoinjcn  22287  txconn  22289  xpstopnlem1  22409  qustgplem  22721  metustid  23156  axlowdim2  26738  axlowdim  26739  axcontlem2  26743  axcontlem3  26744  axcontlem4  26745  axcontlem9  26750  axcontlem10  26751  axcontlem11  26752  cusgrexg  27218  rgrusgrprc  27363  2clwwlk2clwwlk  28121  isnvlem  28379  br8d  30353  prsdm  31145  eulerpartlemgvv  31622  reprsuc  31874  bnj941  32032  bnj944  32198  cvmlift2lem1  32537  cvmlift2lem12  32549  goel  32582  gonafv  32585  satf0op  32612  sat1el2xp  32614  fmla0xp  32618  sategoelfvb  32654  br8  32980  br6  32981  br4  32982  dfrn5  33005  elima4  33007  pprodss4v  33333  brimg  33386  brapply  33387  brsuccf  33390  brrestrict  33398  dfrdg4  33400  cgrtriv  33451  brofs  33454  segconeu  33460  btwntriv2  33461  transportprops  33483  brifs  33492  ifscgr  33493  brcgr3  33495  cgrxfr  33504  brcolinear2  33507  colineardim1  33510  brfs  33528  idinside  33533  btwnconn1lem7  33542  btwnconn1lem11  33546  btwnconn1lem12  33547  btwnconn1lem14  33549  brsegle  33557  seglerflx  33561  seglemin  33562  segleantisym  33564  btwnsegle  33566  outsideofeu  33580  outsidele  33581  linedegen  33592  fvline  33593  finxpreclem6  34664  finxpsuclem  34665  curfv  34859  poimirlem4  34883  poimirlem26  34905  isdivrngo  35215  drngoi  35216  iss2  35588  dibelval3  38270  diblsmopel  38294  dihjatcclem4  38544  frlmsnic  39134  dfhe3  40106  dffrege115  40309  dropab2  40765  relopabVD  41220  projf1o  41443  sge0xp  42696  hoidmv1le  42861  ichnreuop  43619  ichreuopeq  43620  reuopreuprim  43673  prelrrx2b  44686  rrx2xpref1o  44690  rrx2plordisom  44695
 Copyright terms: Public domain W3C validator