Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-gabss Structured version   Visualization version   GIF version

Theorem bj-gabss 36641
Description: Inclusion of generalized class abstractions. (Contributed by BJ, 4-Oct-2024.)
Assertion
Ref Expression
bj-gabss (∀𝑥(𝐴 = 𝐵 ∧ (𝜑𝜓)) → {𝐴𝑥𝜑} ⊆ {𝐵𝑥𝜓})

Proof of Theorem bj-gabss
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eqeq1 2730 . . . . . . . 8 (𝐴 = 𝐵 → (𝐴 = 𝑦𝐵 = 𝑦))
21biimpd 228 . . . . . . 7 (𝐴 = 𝐵 → (𝐴 = 𝑦𝐵 = 𝑦))
32adantr 479 . . . . . 6 ((𝐴 = 𝐵 ∧ (𝜑𝜓)) → (𝐴 = 𝑦𝐵 = 𝑦))
4 simpr 483 . . . . . 6 ((𝐴 = 𝐵 ∧ (𝜑𝜓)) → (𝜑𝜓))
53, 4anim12d 607 . . . . 5 ((𝐴 = 𝐵 ∧ (𝜑𝜓)) → ((𝐴 = 𝑦𝜑) → (𝐵 = 𝑦𝜓)))
65aleximi 1827 . . . 4 (∀𝑥(𝐴 = 𝐵 ∧ (𝜑𝜓)) → (∃𝑥(𝐴 = 𝑦𝜑) → ∃𝑥(𝐵 = 𝑦𝜓)))
76alrimiv 1923 . . 3 (∀𝑥(𝐴 = 𝐵 ∧ (𝜑𝜓)) → ∀𝑦(∃𝑥(𝐴 = 𝑦𝜑) → ∃𝑥(𝐵 = 𝑦𝜓)))
8 ss2ab 4056 . . 3 ({𝑦 ∣ ∃𝑥(𝐴 = 𝑦𝜑)} ⊆ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)} ↔ ∀𝑦(∃𝑥(𝐴 = 𝑦𝜑) → ∃𝑥(𝐵 = 𝑦𝜓)))
97, 8sylibr 233 . 2 (∀𝑥(𝐴 = 𝐵 ∧ (𝜑𝜓)) → {𝑦 ∣ ∃𝑥(𝐴 = 𝑦𝜑)} ⊆ {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)})
10 df-bj-gab 36640 . 2 {𝐴𝑥𝜑} = {𝑦 ∣ ∃𝑥(𝐴 = 𝑦𝜑)}
11 df-bj-gab 36640 . 2 {𝐵𝑥𝜓} = {𝑦 ∣ ∃𝑥(𝐵 = 𝑦𝜓)}
129, 10, 113sstr4g 4025 1 (∀𝑥(𝐴 = 𝐵 ∧ (𝜑𝜓)) → {𝐴𝑥𝜑} ⊆ {𝐵𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1532   = wceq 1534  wex 1774  {cab 2703  wss 3947  {bj-cgab 36639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ss 3964  df-bj-gab 36640
This theorem is referenced by:  bj-gabssd  36642
  Copyright terms: Public domain W3C validator