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

Theorem opeq2 3597
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 2145 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 452 . . . . 5 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 eqidd 2084 . . . . . . 7 (𝐴 = 𝐵 → {𝐶} = {𝐶})
4 preq2 3494 . . . . . . 7 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
53, 4preq12d 3501 . . . . . 6 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
65eleq2d 2152 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
72, 6anbi12d 457 . . . 4 (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
8 df-3an 922 . . . 4 ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}))
9 df-3an 922 . . . 4 ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
107, 8, 93bitr4g 221 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
1110abbidv 2200 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
12 df-op 3431 . 2 𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
13 df-op 3431 . 2 𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
1411, 12, 133eqtr4g 2140 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920   = wceq 1285  wcel 1434  {cab 2069  Vcvv 2612  {csn 3422  {cpr 3423  cop 3425
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-v 2614  df-un 2988  df-sn 3428  df-pr 3429  df-op 3431
This theorem is referenced by:  opeq12  3598  opeq2i  3600  opeq2d  3603  oteq2  3606  oteq3  3607  breq2  3815  cbvopab2  3878  cbvopab2v  3881  opthg  4029  eqvinop  4034  opelopabsb  4051  opelxp  4430  opabid2  4525  elrn2g  4584  opeldm  4597  opeldmg  4599  elrn2  4635  opelresg  4678  iss  4715  elimasng  4755  issref  4769  dmsnopg  4856  cnvsng  4870  elxp4  4872  elxp5  4873  dffun5r  4981  funopg  5001  f1osng  5242  tz6.12f  5278  fsn  5411  fsng  5412  fvsng  5435  oveq2  5599  cbvoprab2  5656  ovg  5718  opabex3d  5827  opabex3  5828  op1stg  5856  op2ndg  5857  op1steq  5884  dfoprab4f  5898  tfrlemibxssdm  6024  tfr1onlembxssdm  6040  tfrcllembxssdm  6053  mapsnen  6458  xpsnen  6467  xpassen  6476  xpf1o  6490  djulclr  6648  djurclr  6649  djulcl  6650  djurcl  6651  djulclb  6654  djur  6664  djuss  6668  1stinl  6672  2ndinl  6673  1stinr  6674  2ndinr  6675  elreal  7269  ax1rid  7315  fseq1p1m1  9401  djucllem  11043
  Copyright terms: Public domain W3C validator