Theorem opeq2 4818

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 2825	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		preq2 4679	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
4	3	preq2d 4685	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
5	2, 4	ifbieq1d 4492	. 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅))
6		dfopif 4814	. 2 ⊢ ⟨𝐶, 𝐴⟩ = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅)
7		dfopif 4814	. 2 ⊢ ⟨𝐶, 𝐵⟩ = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)
8	5, 6, 7	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  ifcif 4467  {csn 4568  {cpr 4570  ⟨cop 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  opeq12  4819  opeq2i  4821  opeq2d  4824  oteq2  4827  oteq3  4828  breq2  5090  cbvopab2  5162  cbvopab2v  5165  opthg  5426  eqvinop  5436  opelopabsb  5479  dfid3  5523  opelxp  5661  relopabi  5772  opabid2  5778  elrn2g  5840  opeldmd  5856  opeldm  5857  iss  5995  elidinxp  6004  dmsnopg  6172  reuop  6252  funopg  6527  f1osng  6817  f1oprswap  6820  tz6.12f  6860  fvn0ssdmfun  7021  fsn  7083  fsng  7085  fprg  7103  fprb  7143  oveq2  7369  cbvoprab2  7449  cbvoprab3v  7453  ovg  7526  elxp4  7867  elxp5  7868  opabex3d  7912  opabex3rd  7913  opabex3  7914  op1stg  7948  op2ndg  7949  op1steq  7980  dfoprab4f  8003  fsplit  8061  xpord2pred  8089  seqomlem2  8384  omeu  8514  oeeui  8532  ralxpmap  8838  elixpsn  8879  ixpsnf1o  8880  mapsnend  8977  xpsnen  8993  xpassen  9003  xpf1o  9071  unxpdomlem1  9160  djulcl  9828  djurcl  9829  djur  9837  djuss  9838  djuun  9844  1stinl  9845  2ndinl  9846  1stinr  9847  2ndinr  9848  axdc4lem  10371  nqereu  10846  mulcanenq  10877  elreal  11048  ax1rid  11078  fseq1p1m1  13546  pfxval  14630  swrdccatin1  14681  swrdccat3blem  14695  wrdlen2  14900  ruclem1  16192  imasaddfnlem  17486  imasvscafn  17495  catidex  17634  catpropd  17669  funcsetcestrclem1  18114  symg2bas  19362  efgi  19688  gsumcom2  19944  pzriprnglem3  21476  pzriprnglem10  21483  mat1rhmval  22457  mat1ric  22465  txkgen  23630  cnmpt21  23649  xkoinjcn  23665  txconn  23667  xpstopnlem1  23787  qustgplem  24099  metustid  24532  axlowdim2  29046  axlowdim  29047  axcontlem2  29051  axcontlem3  29052  axcontlem4  29053  axcontlem9  29058  axcontlem10  29059  axcontlem11  29060  cusgrexg  29530  rgrusgrprc  29676  2clwwlk2clwwlk  30438  isnvlem  30699  br8d  32699  gsumhashmul  33146  prsdm  34077  eulerpartlemgvv  34539  reprsuc  34778  bnj941  34934  bnj944  35099  fineqvrep  35277  cvmlift2lem1  35503  cvmlift2lem12  35515  goel  35548  gonafv  35551  satf0op  35578  sat1el2xp  35580  fmla0xp  35584  sategoelfvb  35620  br8  35957  br6  35958  br4  35959  dfrn5  35975  elima4  35977  pprodss4v  36083  brimg  36136  brapply  36137  lemsuccf  36140  brrestrict  36150  dfrdg4  36152  cgrtriv  36203  brofs  36206  segconeu  36212  btwntriv2  36213  transportprops  36235  brifs  36244  ifscgr  36245  brcgr3  36247  cgrxfr  36256  brcolinear2  36259  colineardim1  36262  brfs  36280  idinside  36285  btwnconn1lem7  36294  btwnconn1lem11  36298  btwnconn1lem12  36299  btwnconn1lem14  36301  brsegle  36309  seglerflx  36313  seglemin  36314  segleantisym  36316  btwnsegle  36318  outsideofeu  36332  outsidele  36333  linedegen  36344  fvline  36345  cbvoprab2vw  36439  cbvoprab23vw  36441  cbvopab2davw  36466  cbvoprab2davw  36473  finxpreclem6  37729  finxpsuclem  37730  curfv  37938  poimirlem4  37962  poimirlem26  37984  isdivrngo  38288  drngoi  38289  iss2  38682  dibelval3  41610  diblsmopel  41634  dihjatcclem4  41884  frlmsnic  43002  dfhe3  44223  dffrege115  44426  dropab2  44895  relopabVD  45348  projf1o  45647  sge0xp  46878  hoidmv1le  47043  fsetsniunop  47512  fsetsnf  47514  fsetsnf1  47515  fsetsnfo  47516  ichnreuop  47947  ichreuopeq  47948  reuopreuprim  48001  gpgprismgriedgdmss  48543  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx0  48552  gpgedgvtx1  48553  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  gpg3kgrtriexlem6  48579  gpgprismgr4cycllem3  48588  pgnbgreunbgrlem1  48604  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  pgnbgreunbgrlem5  48614  gpg5edgnedg  48621  0aryfvalel  49125  1arymaptf1  49133  2arymaptf1  49144  prelrrx2b  49205  rrx2xpref1o  49209  rrx2plordisom  49214  sectpropdlem  49526  ssccatid  49562  isthincd2lem2  49925