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

Theorem opeq2 3777
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 2240 . . . . . 6 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi2d 464 . . . . 5 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V)))
3 eqidd 2178 . . . . . . 7 (𝐴 = 𝐵 → {𝐶} = {𝐶})
4 preq2 3669 . . . . . . 7 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
53, 4preq12d 3676 . . . . . 6 (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}})
65eleq2d 2247 . . . . 5 (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
72, 6anbi12d 473 . . . 4 (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
8 df-3an 980 . . . 4 ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}))
9 df-3an 980 . . . 4 ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))
107, 8, 93bitr4g 223 . . 3 (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})))
1110abbidv 2295 . 2 (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})})
12 df-op 3600 . 2 𝐶, 𝐴⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})}
13 df-op 3600 . 2 𝐶, 𝐵⟩ = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}
1411, 12, 133eqtr4g 2235 1 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978   = wceq 1353  wcel 2148  {cab 2163  Vcvv 2737  {csn 3591  {cpr 3592  cop 3594
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600
This theorem is referenced by:  opeq12  3778  opeq2i  3780  opeq2d  3783  oteq2  3786  oteq3  3787  breq2  4004  cbvopab2  4074  cbvopab2v  4077  opthg  4235  eqvinop  4240  opelopabsb  4257  opelxp  4653  opabid2  4754  elrn2g  4813  opeldm  4826  opeldmg  4828  elrn2  4865  opelresg  4910  iss  4949  elimasng  4992  issref  5007  dmsnopg  5096  cnvsng  5110  elxp4  5112  elxp5  5113  dffun5r  5224  funopg  5246  f1osng  5498  tz6.12f  5540  fsn  5684  fsng  5685  fvsng  5708  oveq2  5877  cbvoprab2  5942  ovg  6007  opabex3d  6116  opabex3  6117  op1stg  6145  op2ndg  6146  oprssdmm  6166  op1steq  6174  dfoprab4f  6188  tfrlemibxssdm  6322  tfr1onlembxssdm  6338  tfrcllembxssdm  6351  elixpsn  6729  ixpsnf1o  6730  mapsnen  6805  xpsnen  6815  xpassen  6824  xpf1o  6838  djulclr  7042  djurclr  7043  djulcl  7044  djurcl  7045  djulclb  7048  inl11  7058  djuss  7063  1stinl  7067  2ndinl  7068  1stinr  7069  2ndinr  7070  elreal  7818  ax1rid  7867  fseq1p1m1  10080  cnmpt21  13458  djucllem  14208
  Copyright terms: Public domain W3C validator