MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supeq1 Structured version   Visualization version   GIF version

Theorem supeq1 9377
Description: Equality theorem for supremum. (Contributed by NM, 22-May-1999.)
Assertion
Ref Expression
supeq1 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Proof of Theorem supeq1
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 raleq 3307 . . . . 5 (𝐵 = 𝐶 → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦𝐶 ¬ 𝑥𝑅𝑦))
2 rexeq 3308 . . . . . . 7 (𝐵 = 𝐶 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐶 𝑦𝑅𝑧))
32imbi2d 340 . . . . . 6 (𝐵 = 𝐶 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
43ralbidv 3172 . . . . 5 (𝐵 = 𝐶 → (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
51, 4anbi12d 631 . . . 4 (𝐵 = 𝐶 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))))
65rabbidv 3413 . . 3 (𝐵 = 𝐶 → {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))})
76unieqd 4877 . 2 (𝐵 = 𝐶 {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))})
8 df-sup 9374 . 2 sup(𝐵, 𝐴, 𝑅) = {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))}
9 df-sup 9374 . 2 sup(𝐶, 𝐴, 𝑅) = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))}
107, 8, 93eqtr4g 2801 1 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396   = wceq 1541  wral 3062  wrex 3071  {crab 3405   cuni 4863   class class class wbr 5103  supcsup 9372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-in 3915  df-ss 3925  df-uni 4864  df-sup 9374
This theorem is referenced by:  supeq1d  9378  supeq1i  9379  infeq1  9408  bndth  24305  ioorval  24922  uniioombllem6  24936  mdegcl  25418  limexissupab  41556  suplesup  43509  supminfxr  43635  prproropf1olem2  45628  prproropf1olem3  45629  prproropf1olem4  45630  prproropf1o  45631  prproropreud  45633
  Copyright terms: Public domain W3C validator