Theorem opeq1 4845

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 2852	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 643	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4594	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4696	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4704	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4510	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4842	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4842	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  ifcif 4485  {csn 4588  {cpr 4590  ⟨cop 4840

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841

This theorem is used by:  opeq12  4847  opeq1i  4848  opeq1d  4851  oteq1  4865  breq1  5111  cbvopab1  5185  cbvopab1g  5186  cbvopab1s  5188  cbvopab1v  5189  opthg  5453  eqvinop  5463  sbcop1  5465  opelopabsb  5511  opelxp  5694  elvvv  5735  opabid2  5816  opeliunxp2  5825  el2xptp  5830  elsnres  6028  dmsnopg  6233  reuop  6322  funopg  6602  f1osng  6898  f1oprswap  6901  dmfco  7012  fvelrn  7108  fsng  7170  funsneqopb  7188  fprg  7191  fvrnressn  7197  funfvima3  7273  oveq1  7458  oprabidw  7482  oprabid  7483  dfoprab2  7509  cbvoprab1  7538  elxp4  7968  elxp5  7969  opabex3d  8011  opabex3rd  8012  opabex3  8013  op1stg  8047  op2ndg  8048  dfoprab4f  8102  frxp  8175  frxp2  8198  xpord2pred  8199  opeliunxp2f  8265  tfrlem11  8434  omeu  8631  oeeui  8649  curfv  8930  elixpsn  9003  fundmen  9097  xpsnen  9118  xpassen  9128  xpf1o  9196  unxpdomlem1  9285  djur  10037  dfac5lem1  10241  dfac5lem4  10244  axdc4lem  10572  nqereu  11053  mulcanenq  11084  archnq  11104  prlem934  11157  supsrlem  11235  supsr  11236  swrdccatin1  14916  swrdccat3blem  14930  fsum2dlem  15980  fprod2dlem  16191  vdwlem10  17212  imasaddfnlem  17750  catideu  17899  iscatd2  17905  catlid  17907  catpropd  17933  degenmgm2nfun  19189  symg2bas  19658  efgmval  19977  efgi  19984  vrgpval  20032  gsumcom2  20240  rngqiprngimfo  21648  pzriprnglem10  21851  pzriprnglem11  21852  txkgen  24026  cnmpt21  24045  xkoinjcn  24061  txconn  24063  pt1hmeo  24180  cnextfvval  24439  qustgplem  24495  dvbsss  26277  axlowdim2  29595  axlowdim  29596  axcontlem10  29608  axcontlem12  29610  isnvlem  31269  br8d  33300  2ndresdju  33341  gsumhashmul  33727  gsumwrd2dccatlem  33737  rlocf1  33934  idomsubr  33975  prsrn  34658  esum2dlem  34835  eulerpartlemgvv  35119  omeueq  35837  soinfdom  35841  fineqvrep  35923  gdlopcfv1  36013  gdlopcfv2  36014  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  j0le  36060  k3n0j0lt  36061  jltaleph  36067  satf0op  36350  satffunlem1lem1  36375  satffunlem2lem1  36377  sategoelfvb  36392  br8  36736  br6  36737  br4  36738  eldm3  36741  dfdm5  36752  elfuns  36892  brimg  36914  brapply  36915  lemsuccf  36918  brrestrict  36928  dfrdg4  36930  cgrdegen  36984  brofs  36985  cgrextend  36988  brifs  37023  ifscgr  37024  brcgr3  37026  brcolinear2  37038  colineardim1  37041  brfs  37059  idinside  37064  btwnconn1lem7  37073  btwnconn1lem11  37077  btwnconn1lem12  37078  brsegle  37088  outsideofeu  37111  fvray  37121  linedegen  37123  fvline  37124  cbvoprab1vw  37241  cbvoprab13vw  37245  cbvopab1davw  37268  cbvoprab1davw  37275  bj-inftyexpiinv  38397  bj-inftyexpidisj  38399  finxpeq2  38578  finxpreclem6  38587  finxpsuclem  38588  isdivrngo  39150  drngoi  39151  dicelval3  42503  dihjatcclem4  42744  dropab1  45690  relopabVD  46143  funressndmafv2rn  48566  dfatdmfcoafv2  48597  ichnreuop  48827  ichreuopeq  48828  reuopreuprim  48881  gpgedgvtx0  49432  gpgedgvtx1  49433  gpgcubic  49450  gpg5nbgr3star  49452  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  pgnbgreunbgr  49496  sectpropdlem  50481  ssccatid  50517  upfval2  50624  isthincd2lem2  50901  fuconuniqex2  51118