Theorem opeq1 4839

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 2848	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 643	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4590	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4690	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4698	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4506	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4836	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4836	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ∅c0 4278  ifcif 4481  {csn 4584  {cpr 4586  ⟨cop 4834

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  opeq12  4841  opeq1i  4842  opeq1d  4845  oteq1  4859  breq1  5105  cbvopab1  5178  cbvopab1g  5179  cbvopab1s  5181  cbvopab1v  5182  opthg  5445  eqvinop  5455  sbcop1  5457  opelopabsb  5503  opelxp  5686  elvvv  5726  opabid2  5805  opeliunxp2  5814  el2xptp  5819  elsnres  6009  dmsnopg  6214  reuop  6296  funopg  6575  f1osng  6868  f1oprswap  6871  dmfco  6982  fvelrn  7077  fsng  7139  funsneqopb  7157  fprg  7160  fvrnressn  7166  funfvima3  7243  oveq1  7428  oprabidw  7452  oprabid  7453  dfoprab2  7479  cbvoprab1  7508  elxp4  7935  elxp5  7936  opabex3d  7978  opabex3rd  7979  opabex3  7980  op1stg  8014  op2ndg  8015  dfoprab4f  8068  frxp  8141  frxp2  8164  xpord2pred  8165  opeliunxp2f  8231  tfrlem11  8400  omeu  8597  oeeui  8615  curfv  8896  elixpsn  8969  fundmen  9063  xpsnen  9084  xpassen  9094  xpf1o  9162  unxpdomlem1  9251  djur  10004  dfac5lem1  10206  dfac5lem4  10209  axdc4lem  10537  nqereu  11018  mulcanenq  11049  archnq  11069  prlem934  11122  supsrlem  11200  supsr  11201  swrdccatin1  14879  swrdccat3blem  14893  fsum2dlem  15942  fprod2dlem  16153  vdwlem10  17174  imasaddfnlem  17706  catideu  17855  iscatd2  17861  catlid  17863  catpropd  17889  degenmgm2nfun  19145  symg2bas  19613  efgmval  19932  efgi  19939  vrgpval  19987  gsumcom2  20195  rngqiprngimfo  21603  pzriprnglem10  21802  pzriprnglem11  21803  txkgen  23977  cnmpt21  23996  xkoinjcn  24012  txconn  24014  pt1hmeo  24131  cnextfvval  24390  qustgplem  24446  dvbsss  26228  axlowdim2  29544  axlowdim  29545  axcontlem10  29557  axcontlem12  29559  isnvlem  31218  br8d  33250  2ndresdju  33291  gsumhashmul  33675  gsumwrd2dccatlem  33685  rlocf1  33882  idomsubr  33918  prsrn  34594  esum2dlem  34771  eulerpartlemgvv  35055  soinfdom  35769  fineqvrep  35839  satf0op  36229  satffunlem1lem1  36254  satffunlem2lem1  36256  sategoelfvb  36271  br8  36614  br6  36615  br4  36616  eldm3  36619  dfdm5  36630  elfuns  36770  brimg  36792  brapply  36793  lemsuccf  36796  brrestrict  36806  dfrdg4  36808  cgrdegen  36862  brofs  36863  cgrextend  36866  brifs  36901  ifscgr  36902  brcgr3  36904  brcolinear2  36916  colineardim1  36919  brfs  36937  idinside  36942  btwnconn1lem7  36951  btwnconn1lem11  36955  btwnconn1lem12  36956  brsegle  36966  outsideofeu  36989  fvray  36999  linedegen  37001  fvline  37002  cbvoprab1vw  37119  cbvoprab13vw  37123  cbvopab1davw  37146  cbvoprab1davw  37153  bj-inftyexpiinv  38223  bj-inftyexpidisj  38225  finxpeq2  38404  finxpreclem6  38413  finxpsuclem  38414  isdivrngo  38978  drngoi  38979  dicelval3  42331  dihjatcclem4  42572  dropab1  45524  relopabVD  45977  funressndmafv2rn  48387  dfatdmfcoafv2  48418  ichnreuop  48648  ichreuopeq  48649  reuopreuprim  48702  gpgedgvtx0  49253  gpgedgvtx1  49254  gpgcubic  49271  gpg5nbgr3star  49273  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  pgnbgreunbgr  49317  sectpropdlem  50244  ssccatid  50280  upfval2  50387  isthincd2lem2  50664  fuconuniqex2  50881