Theorem opeq2 3861

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

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2292	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi2d 464	. . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3		eqidd 2230	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶} = {𝐶})
4		preq2 3747	. . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
5	3, 4	preq12d 3754	. . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
6	5	eleq2d 2299	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
7	2, 6	anbi12d 473	. . . 4 ⊢ (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
8		df-3an 1004	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}))
9		df-3an 1004	. . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
10	7, 8, 9	3bitr4g 223	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
11	10	abbidv 2347	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
12		df-op 3676	. 2 ⊢ ⟨𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
13		df-op 3676	. 2 ⊢ ⟨𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
14	11, 12, 13	3eqtr4g 2287	1 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  {cab 2215  Vcvv 2800  {csn 3667  {cpr 3668  ⟨cop 3670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676

This theorem is referenced by:  opeq12  3862  opeq2i  3864  opeq2d  3867  oteq2  3870  oteq3  3871  breq2  4090  cbvopab2  4161  cbvopab2v  4164  opthg  4328  eqvinop  4333  opelopabsb  4352  opelxp  4753  opabid2  4859  elrn2g  4918  opeldm  4932  opeldmg  4934  elrn2  4972  opelresg  5018  iss  5057  elimasng  5102  issref  5117  dmsnopg  5206  cnvsng  5220  elxp4  5222  elxp5  5223  dffun5r  5336  funopg  5358  f1osng  5622  tz6.12f  5664  fsn  5815  fsng  5816  fvsng  5845  oveq2  6021  cbvoprab2  6089  ovg  6156  opabex3d  6278  opabex3  6279  op1stg  6308  op2ndg  6309  oprssdmm  6329  op1steq  6337  dfoprab4f  6351  elmpom  6398  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  elixpsn  6899  ixpsnf1o  6900  mapsnen  6981  xpsnen  7000  xpassen  7009  xpf1o  7025  djulclr  7239  djurclr  7240  djulcl  7241  djurcl  7242  djulclb  7245  inl11  7255  djuss  7260  1stinl  7264  2ndinl  7265  1stinr  7266  2ndinr  7267  elreal  8038  ax1rid  8087  fseq1p1m1  10319  pfxval  11245  swrdccatin1  11296  swrdccat3blem  11310  imasaddfnlemg  13387  cnmpt21  15005  djucllem  16332