Theorem opeq1 4897

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

Step	Hyp	Ref	Expression
1		eleq1 2832	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4658	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4758	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4766	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4572	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4894	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4894	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  ifcif 4548  {csn 4648  {cpr 4650  ⟨cop 4654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655

This theorem is referenced by:  opeq12  4899  opeq1i  4900  opeq1d  4903  oteq1  4906  breq1  5169  cbvopab1  5241  cbvopab1g  5242  cbvopab1s  5244  cbvopab1v  5245  opthg  5497  eqvinop  5507  sbcop1  5508  opelopabsb  5549  opelxp  5736  elvvv  5775  opabid2  5852  opeliunxp2  5863  elsnres  6050  elimasngOLD  6120  dmsnopg  6244  reuop  6324  funopg  6612  f1osng  6903  f1oprswap  6906  dmfco  7018  fvelrn  7110  fsng  7171  funsneqopb  7186  fprg  7189  fvrnressn  7195  funfvima3  7273  oveq1  7455  oprabidw  7479  oprabid  7480  dfoprab2  7508  cbvoprab1  7537  elxp4  7962  elxp5  7963  opabex3d  8006  opabex3rd  8007  opabex3  8008  op1stg  8042  op2ndg  8043  el2xptp  8076  dfoprab4f  8097  frxp  8167  frxp2  8185  xpord2pred  8186  opeliunxp2f  8251  tfrlem11  8444  omeu  8641  oeeui  8658  elixpsn  8995  fundmen  9096  xpsnen  9121  xpassen  9132  xpf1o  9205  unxpdomlem1  9313  djur  9988  dfac5lem1  10192  dfac5lem4  10195  dfac5lem4OLD  10197  axdc4lem  10524  nqereu  10998  mulcanenq  11029  archnq  11049  prlem934  11102  supsrlem  11180  supsr  11181  swrdccatin1  14773  swrdccat3blem  14787  fsum2dlem  15818  fprod2dlem  16028  vdwlem10  17037  imasaddfnlem  17588  catideu  17733  iscatd2  17739  catlid  17741  catpropd  17767  symg2bas  19434  efgmval  19754  efgi  19761  vrgpval  19809  gsumcom2  20017  rngqiprngimfo  21334  pzriprnglem10  21524  pzriprnglem11  21525  txkgen  23681  cnmpt21  23700  xkoinjcn  23716  txconn  23718  pt1hmeo  23835  cnextfvval  24094  qustgplem  24150  dvbsss  25957  axlowdim2  28993  axlowdim  28994  axcontlem10  29006  axcontlem12  29008  isnvlem  30642  br8d  32632  2ndresdju  32667  cnvoprabOLD  32734  gsumhashmul  33040  rlocf1  33245  idomsubr  33276  prsrn  33861  esum2dlem  34056  eulerpartlemgvv  34341  fineqvrep  35071  satf0op  35345  satffunlem1lem1  35370  satffunlem2lem1  35372  sategoelfvb  35387  br8  35718  br6  35719  br4  35720  eldm3  35723  dfdm5  35736  elfuns  35879  brimg  35901  brapply  35902  brsuccf  35905  brrestrict  35913  dfrdg4  35915  cgrdegen  35968  brofs  35969  cgrextend  35972  brifs  36007  ifscgr  36008  brcgr3  36010  brcolinear2  36022  colineardim1  36025  brfs  36043  idinside  36048  btwnconn1lem7  36057  btwnconn1lem11  36061  btwnconn1lem12  36062  brsegle  36072  outsideofeu  36095  fvray  36105  linedegen  36107  fvline  36108  cbvoprab1vw  36203  cbvoprab13vw  36207  cbvopab1davw  36230  cbvoprab1davw  36237  bj-inftyexpiinv  37174  bj-inftyexpidisj  37176  finxpeq2  37353  finxpreclem6  37362  finxpsuclem  37363  curfv  37560  isdivrngo  37910  drngoi  37911  dicelval3  41137  dihjatcclem4  41378  dropab1  44416  relopabVD  44872  funressndmafv2rn  47138  dfatdmfcoafv2  47169  ichnreuop  47346  ichreuopeq  47347  reuopreuprim  47400  isthincd2lem2  48703