ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opeq2 GIF version

Theorem opeq2 3606
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.
StepHypRef Expression
1 eleq1 2147 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 452 . . . . 5 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 eqidd 2086 . . . . . . 7 (𝐴 = 𝐵 → {𝐶} = {𝐶})
4 preq2 3503 . . . . . . 7 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
53, 4preq12d 3510 . . . . . 6 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
65eleq2d 2154 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
72, 6anbi12d 457 . . . 4 (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
8 df-3an 924 . . . 4 ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}))
9 df-3an 924 . . . 4 ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
107, 8, 93bitr4g 221 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
1110abbidv 2202 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
12 df-op 3440 . 2 𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
13 df-op 3440 . 2 𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
1411, 12, 133eqtr4g 2142 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922   = wceq 1287  wcel 1436  {cab 2071  Vcvv 2615  {csn 3431  {cpr 3432  cop 3434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440
This theorem is referenced by:  opeq12  3607  opeq2i  3609  opeq2d  3612  oteq2  3615  oteq3  3616  breq2  3824  cbvopab2  3887  cbvopab2v  3890  opthg  4038  eqvinop  4043  opelopabsb  4060  opelxp  4439  opabid2  4534  elrn2g  4593  opeldm  4606  opeldmg  4608  elrn2  4644  opelresg  4687  iss  4724  elimasng  4764  issref  4778  dmsnopg  4865  cnvsng  4879  elxp4  4881  elxp5  4882  dffun5r  4990  funopg  5010  f1osng  5251  tz6.12f  5290  fsn  5426  fsng  5427  fvsng  5450  oveq2  5615  cbvoprab2  5672  ovg  5734  opabex3d  5843  opabex3  5844  op1stg  5872  op2ndg  5873  op1steq  5900  dfoprab4f  5914  tfrlemibxssdm  6040  tfr1onlembxssdm  6056  tfrcllembxssdm  6069  mapsnen  6474  xpsnen  6483  xpassen  6492  xpf1o  6506  djulclr  6678  djurclr  6679  djulcl  6680  djurcl  6681  djulclb  6684  djur  6694  djuss  6698  1stinl  6702  2ndinl  6703  1stinr  6704  2ndinr  6705  elreal  7303  ax1rid  7349  fseq1p1m1  9431  djucllem  11130
  Copyright terms: Public domain W3C validator