Theorem opeq1 4820

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 2819	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4581	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4681	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4689	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4495	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4817	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4817	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2791	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436  ∅c0 4278  ifcif 4470  {csn 4571  {cpr 4573  ⟨cop 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578

This theorem is referenced by:  opeq12  4822  opeq1i  4823  opeq1d  4826  oteq1  4829  breq1  5089  cbvopab1  5160  cbvopab1g  5161  cbvopab1s  5163  cbvopab1v  5164  opthg  5412  eqvinop  5422  sbcop1  5423  opelopabsb  5465  opelxp  5647  elvvv  5687  opabid2  5763  opeliunxp2  5773  elsnres  5965  dmsnopg  6155  reuop  6235  funopg  6510  f1osng  6799  f1oprswap  6802  dmfco  6913  fvelrn  7004  fsng  7065  funsneqopb  7080  fprg  7083  fvrnressn  7089  funfvima3  7165  oveq1  7348  oprabidw  7372  oprabid  7373  dfoprab2  7399  cbvoprab1  7428  elxp4  7847  elxp5  7848  opabex3d  7892  opabex3rd  7893  opabex3  7894  op1stg  7928  op2ndg  7929  el2xptp  7962  dfoprab4f  7983  frxp  8051  frxp2  8069  xpord2pred  8070  opeliunxp2f  8135  tfrlem11  8302  omeu  8495  oeeui  8512  elixpsn  8856  fundmen  8948  xpsnen  8969  xpassen  8979  xpf1o  9047  unxpdomlem1  9135  djur  9807  dfac5lem1  10009  dfac5lem4  10012  dfac5lem4OLD  10014  axdc4lem  10341  nqereu  10815  mulcanenq  10846  archnq  10866  prlem934  10919  supsrlem  10997  supsr  10998  swrdccatin1  14627  swrdccat3blem  14641  fsum2dlem  15672  fprod2dlem  15882  vdwlem10  16897  imasaddfnlem  17427  catideu  17576  iscatd2  17582  catlid  17584  catpropd  17610  symg2bas  19300  efgmval  19619  efgi  19626  vrgpval  19674  gsumcom2  19882  rngqiprngimfo  21233  pzriprnglem10  21422  pzriprnglem11  21423  txkgen  23562  cnmpt21  23581  xkoinjcn  23597  txconn  23599  pt1hmeo  23716  cnextfvval  23975  qustgplem  24031  dvbsss  25825  axlowdim2  28933  axlowdim  28934  axcontlem10  28946  axcontlem12  28948  isnvlem  30582  br8d  32583  2ndresdju  32623  gsumhashmul  33033  gsumwrd2dccatlem  33038  rlocf1  33232  idomsubr  33267  prsrn  33920  esum2dlem  34097  eulerpartlemgvv  34381  fineqvrep  35129  satf0op  35413  satffunlem1lem1  35438  satffunlem2lem1  35440  sategoelfvb  35455  br8  35792  br6  35793  br4  35794  eldm3  35797  dfdm5  35809  elfuns  35949  brimg  35971  brapply  35972  brsuccf  35975  brrestrict  35983  dfrdg4  35985  cgrdegen  36038  brofs  36039  cgrextend  36042  brifs  36077  ifscgr  36078  brcgr3  36080  brcolinear2  36092  colineardim1  36095  brfs  36113  idinside  36118  btwnconn1lem7  36127  btwnconn1lem11  36131  btwnconn1lem12  36132  brsegle  36142  outsideofeu  36165  fvray  36175  linedegen  36177  fvline  36178  cbvoprab1vw  36271  cbvoprab13vw  36275  cbvopab1davw  36298  cbvoprab1davw  36305  bj-inftyexpiinv  37242  bj-inftyexpidisj  37244  finxpeq2  37421  finxpreclem6  37430  finxpsuclem  37431  curfv  37640  isdivrngo  37990  drngoi  37991  dicelval3  41219  dihjatcclem4  41460  dropab1  44479  relopabVD  44933  funressndmafv2rn  47254  dfatdmfcoafv2  47285  ichnreuop  47503  ichreuopeq  47504  reuopreuprim  47557  gpgedgvtx0  48092  gpgedgvtx1  48093  gpgcubic  48110  gpg5nbgr3star  48112  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem6  48155  pgnbgreunbgr  48156  sectpropdlem  49068  ssccatid  49104  upfval2  49209  isthincd2lem2  49467