Theorem ecopoveq 8839

Description: This is the first of several theorems about equivalence relations of the kind used in construction of fractions and signed reals, involving operations on equivalent classes of ordered pairs. This theorem expresses the relation ∼ (specified by the hypothesis) in terms of its operation 𝐹. (Contributed by NM, 16-Aug-1995.)

Hypothesis

Ref	Expression
ecopopr.1	⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}

Assertion

Ref	Expression
ecopoveq	⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢, +   𝑥,𝑆,𝑦,𝑧,𝑤,𝑣,𝑢   𝑥,𝐴,𝑦,𝑧,𝑤,𝑣,𝑢   𝑥,𝐵,𝑦,𝑧,𝑤,𝑣,𝑢   𝑥,𝐶,𝑦,𝑧,𝑤,𝑣,𝑢   𝑥,𝐷,𝑦,𝑧,𝑤,𝑣,𝑢

Allowed substitution hints:   ∼ (𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑢)

Proof of Theorem ecopoveq

Step	Hyp	Ref	Expression
1		oveq12 7429	. . . 4 ⊢ ((𝑧 = 𝐴 ∧ 𝑢 = 𝐷) → (𝑧 + 𝑢) = (𝐴 + 𝐷))
2		oveq12 7429	. . . 4 ⊢ ((𝑤 = 𝐵 ∧ 𝑣 = 𝐶) → (𝑤 + 𝑣) = (𝐵 + 𝐶))
3	1, 2	eqeqan12d 2774	. . 3 ⊢ (((𝑧 = 𝐴 ∧ 𝑢 = 𝐷) ∧ (𝑤 = 𝐵 ∧ 𝑣 = 𝐶)) → ((𝑧 + 𝑢) = (𝑤 + 𝑣) ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))
4	3	an42s 674	. 2 ⊢ (((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ (𝑣 = 𝐶 ∧ 𝑢 = 𝐷)) → ((𝑧 + 𝑢) = (𝑤 + 𝑣) ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))
5		ecopopr.1	. 2 ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
6	4, 5	opbrop 5748	1 ⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (⟨𝐴, 𝐵⟩ ∼ ⟨𝐶, 𝐷⟩ ↔ (𝐴 + 𝐷) = (𝐵 + 𝐶)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ⟨cop 4589   class class class wbr 5102  {copab 5166   × cxp 5648  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  ecopovsym  8840  ecopovtrn  8841  ecopover  8842  enqbreq  11004  enrbreq  11150  prsrlem1  11157