Theorem opeq1 4873

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 2829	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4636	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4733	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4741	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4550	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4870	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4870	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  ifcif 4525  {csn 4626  {cpr 4628  ⟨cop 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633

This theorem is referenced by:  opeq12  4875  opeq1i  4876  opeq1d  4879  oteq1  4882  breq1  5146  cbvopab1  5217  cbvopab1g  5218  cbvopab1s  5220  cbvopab1v  5221  opthg  5482  eqvinop  5492  sbcop1  5493  opelopabsb  5535  opelxp  5721  elvvv  5761  opabid2  5838  opeliunxp2  5849  elsnres  6039  dmsnopg  6233  reuop  6313  funopg  6600  f1osng  6889  f1oprswap  6892  dmfco  7005  fvelrn  7096  fsng  7157  funsneqopb  7172  fprg  7175  fvrnressn  7181  funfvima3  7256  oveq1  7438  oprabidw  7462  oprabid  7463  dfoprab2  7491  cbvoprab1  7520  elxp4  7944  elxp5  7945  opabex3d  7990  opabex3rd  7991  opabex3  7992  op1stg  8026  op2ndg  8027  el2xptp  8060  dfoprab4f  8081  frxp  8151  frxp2  8169  xpord2pred  8170  opeliunxp2f  8235  tfrlem11  8428  omeu  8623  oeeui  8640  elixpsn  8977  fundmen  9071  xpsnen  9095  xpassen  9106  xpf1o  9179  unxpdomlem1  9286  djur  9959  dfac5lem1  10163  dfac5lem4  10166  dfac5lem4OLD  10168  axdc4lem  10495  nqereu  10969  mulcanenq  11000  archnq  11020  prlem934  11073  supsrlem  11151  supsr  11152  swrdccatin1  14763  swrdccat3blem  14777  fsum2dlem  15806  fprod2dlem  16016  vdwlem10  17028  imasaddfnlem  17573  catideu  17718  iscatd2  17724  catlid  17726  catpropd  17752  symg2bas  19410  efgmval  19730  efgi  19737  vrgpval  19785  gsumcom2  19993  rngqiprngimfo  21311  pzriprnglem10  21501  pzriprnglem11  21502  txkgen  23660  cnmpt21  23679  xkoinjcn  23695  txconn  23697  pt1hmeo  23814  cnextfvval  24073  qustgplem  24129  dvbsss  25937  axlowdim2  28975  axlowdim  28976  axcontlem10  28988  axcontlem12  28990  isnvlem  30629  br8d  32622  2ndresdju  32659  gsumhashmul  33064  gsumwrd2dccatlem  33069  rlocf1  33277  idomsubr  33311  prsrn  33914  esum2dlem  34093  eulerpartlemgvv  34378  fineqvrep  35109  satf0op  35382  satffunlem1lem1  35407  satffunlem2lem1  35409  sategoelfvb  35424  br8  35756  br6  35757  br4  35758  eldm3  35761  dfdm5  35773  elfuns  35916  brimg  35938  brapply  35939  brsuccf  35942  brrestrict  35950  dfrdg4  35952  cgrdegen  36005  brofs  36006  cgrextend  36009  brifs  36044  ifscgr  36045  brcgr3  36047  brcolinear2  36059  colineardim1  36062  brfs  36080  idinside  36085  btwnconn1lem7  36094  btwnconn1lem11  36098  btwnconn1lem12  36099  brsegle  36109  outsideofeu  36132  fvray  36142  linedegen  36144  fvline  36145  cbvoprab1vw  36238  cbvoprab13vw  36242  cbvopab1davw  36265  cbvoprab1davw  36272  bj-inftyexpiinv  37209  bj-inftyexpidisj  37211  finxpeq2  37388  finxpreclem6  37397  finxpsuclem  37398  curfv  37607  isdivrngo  37957  drngoi  37958  dicelval3  41182  dihjatcclem4  41423  dropab1  44466  relopabVD  44921  funressndmafv2rn  47235  dfatdmfcoafv2  47266  ichnreuop  47459  ichreuopeq  47460  reuopreuprim  47513  gpgedgvtx0  48019  gpgedgvtx1  48020  gpgcubic  48035  gpg5nbgr3star  48037  upfval2  48934  isthincd2lem2  49084