Theorem opeq2 4839

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opeq2	⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Proof of Theorem opeq2

Step	Hyp	Ref	Expression
1		eleq1 2851	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 641	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4700	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4706	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4512	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4835	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4835	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  ifcif 4487  {csn 4589  {cpr 4591  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  opeq12  4840  opeq2i  4842  opeq2d  4845  oteq2  4848  oteq3  4849  breq2  5113  cbvopab2  5187  cbvopab2v  5190  opthg  5459  eqvinop  5469  opelopabsb  5514  dfid3  5559  opelxp  5697  relopabi  5809  opabid2  5815  elrn2g  5880  opeldmd  5896  opeldm  5897  iss  6037  elidinxp  6046  dmsnopg  6214  reuop  6294  funopg  6570  f1osng  6863  f1oprswap  6866  tz6.12f  6906  fvn0ssdmfun  7069  fsn  7131  fsng  7133  fprg  7152  fprb  7192  oveq2  7418  cbvoprab2  7498  cbvoprab3v  7502  ovg  7575  elxp4  7915  elxp5  7916  opabex3d  7958  opabex3rd  7959  opabex3  7960  op1stg  7994  op2ndg  7995  op1steq  8026  dfoprab4f  8049  fsplit  8108  xpord2pred  8137  seqomlem2  8434  omeu  8566  oeeui  8584  ralxpmap  8890  elixpsn  8931  ixpsnf1o  8932  mapsnend  9029  xpsnen  9045  xpassen  9055  xpf1o  9123  unxpdomlem1  9212  djulcl  9892  djurcl  9893  djur  9901  djuss  9902  djuun  9908  1stinl  9909  2ndinl  9910  1stinr  9911  2ndinr  9912  axdc4lem  10434  nqereu  10909  mulcanenq  10940  elreal  11111  ax1rid  11141  fseq1p1m1  13622  pfxval  14707  swrdccatin1  14758  swrdccat3blem  14772  wrdlen2  14977  ruclem1  16282  imasaddfnlem  17577  imasvscafn  17586  catidex  17725  catpropd  17760  funcsetcestrclem1  18205  symg2bas  19458  efgi  19784  gsumcom2  20040  pzriprnglem3  21633  pzriprnglem10  21640  mat1rhmval  22636  mat1ric  22644  txkgen  23809  cnmpt21  23828  xkoinjcn  23844  txconn  23846  xpstopnlem1  23966  qustgplem  24278  metustid  24711  axlowdim2  29310  axlowdim  29311  axcontlem2  29315  axcontlem3  29316  axcontlem4  29317  axcontlem9  29322  axcontlem10  29323  axcontlem11  29324  cusgrexg  29794  rgrusgrprc  29939  2clwwlk2clwwlk  30701  isnvlem  30962  br8d  32953  gsumhashmul  33387  prsdm  34304  eulerpartlemgvv  34766  reprsuc  35002  bnj941  35161  bnj944  35326  fineqvrep  35527  cvmlift2lem1  35794  cvmlift2lem12  35806  goel  35839  gonafv  35842  satf0op  35869  sat1el2xp  35871  fmla0xp  35875  sategoelfvb  35911  br8  36248  br6  36249  br4  36250  dfrn5  36266  elima4  36268  pprodss4v  36374  brimg  36427  brapply  36428  lemsuccf  36431  brrestrict  36441  dfrdg4  36443  cgrtriv  36494  brofs  36497  segconeu  36503  btwntriv2  36504  transportprops  36526  brifs  36535  ifscgr  36536  brcgr3  36538  cgrxfr  36547  brcolinear2  36550  colineardim1  36553  brfs  36571  idinside  36576  btwnconn1lem7  36585  btwnconn1lem11  36589  btwnconn1lem12  36590  btwnconn1lem14  36592  brsegle  36600  seglerflx  36604  seglemin  36605  segleantisym  36607  btwnsegle  36609  outsideofeu  36623  outsidele  36624  linedegen  36635  fvline  36636  cbvoprab2vw  36750  cbvoprab23vw  36752  cbvopab2davw  36777  cbvoprab2davw  36784  finxpreclem6  38042  finxpsuclem  38043  curfv  38251  poimirlem4  38275  poimirlem26  38297  isdivrngo  38601  drngoi  38602  iss2  38993  dibelval3  41921  diblsmopel  41945  dihjatcclem4  42195  frlmsnic  43308  dfhe3  44501  dffrege115  44704  dropab2  45157  relopabVD  45609  projf1o  45914  sge0xp  47143  hoidmv1le  47308  fsetsniunop  47786  fsetsnf  47788  fsetsnf1  47789  fsetsnfo  47790  ichnreuop  48221  ichreuopeq  48222  reuopreuprim  48275  gpgprismgriedgdmss  48817  gpgvtx0  48818  gpgvtx1  48819  gpgedgvtx0  48826  gpgedgvtx1  48827  gpgedgiov  48830  gpgedg2ov  48831  gpgedg2iv  48832  gpg3kgrtriexlem6  48853  gpgprismgr4cycllem3  48862  pgnbgreunbgrlem1  48878  pgnbgreunbgrlem2  48882  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5lem3  48887  pgnbgreunbgrlem5  48888  gpg5edgnedg  48895  0aryfvalel  49414  1arymaptf1  49422  2arymaptf1  49433  prelrrx2b  49494  rrx2xpref1o  49498  rrx2plordisom  49503  sectpropdlem  49814  ssccatid  49850  isthincd2lem2  50213