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

Theorem supeq1 9388
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 3312 . . . . 5 (𝐵 = 𝐶 → (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ↔ ∀𝑦𝐶 ¬ 𝑥𝑅𝑦))
2 rexeq 3313 . . . . . . 7 (𝐵 = 𝐶 → (∃𝑧𝐵 𝑦𝑅𝑧 ↔ ∃𝑧𝐶 𝑦𝑅𝑧))
32imbi2d 341 . . . . . 6 (𝐵 = 𝐶 → ((𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
43ralbidv 3175 . . . . 5 (𝐵 = 𝐶 → (∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧) ↔ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧)))
51, 4anbi12d 632 . . . 4 (𝐵 = 𝐶 → ((∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)) ↔ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))))
65rabbidv 3418 . . 3 (𝐵 = 𝐶 → {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))})
76unieqd 4884 . 2 (𝐵 = 𝐶 {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))} = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))})
8 df-sup 9385 . 2 sup(𝐵, 𝐴, 𝑅) = {𝑥𝐴 ∣ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))}
9 df-sup 9385 . 2 sup(𝐶, 𝐴, 𝑅) = {𝑥𝐴 ∣ (∀𝑦𝐶 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐶 𝑦𝑅𝑧))}
107, 8, 93eqtr4g 2802 1 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wral 3065  wrex 3074  {crab 3410   cuni 4870   class class class wbr 5110  supcsup 9383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-in 3922  df-ss 3932  df-uni 4871  df-sup 9385
This theorem is referenced by:  supeq1d  9389  supeq1i  9390  infeq1  9419  bndth  24337  ioorval  24954  uniioombllem6  24968  mdegcl  25450  limexissupab  41647  suplesup  43647  supminfxr  43773  prproropf1olem2  45770  prproropf1olem3  45771  prproropf1olem4  45772  prproropf1o  45773  prproropreud  45775
  Copyright terms: Public domain W3C validator