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

Theorem ss2abdv 3991
 Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2113, ax-10 2142, ax-11 2158, ax-12 2175. (Revised by Gino Giotto, 28-Jun-2024.)
Hypothesis
Ref Expression
ss2abdv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ss2abdv (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem ss2abdv
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-in 3888 . . 3 ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
2 df-clab 2777 . . . . . . 7 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
32bicomi 227 . . . . . 6 ([𝑦 / 𝑥]𝜓𝑦 ∈ {𝑥𝜓})
4 df-clab 2777 . . . . . . 7 (𝑦 ∈ {𝑥𝜒} ↔ [𝑦 / 𝑥]𝜒)
54bicomi 227 . . . . . 6 ([𝑦 / 𝑥]𝜒𝑦 ∈ {𝑥𝜒})
63, 5anbi12i 629 . . . . 5 (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒}))
76abbii 2863 . . . 4 {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
8 sbequ 2088 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9 sbequ 2088 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
108, 9anbi12d 633 . . . . . . . 8 (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1110sbievw 2100 . . . . . . 7 ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12 ax-1 6 . . . . . . . . . 10 ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
1312a1i 11 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
1413impd 414 . . . . . . . 8 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15 ss2abdv.1 . . . . . . . . . 10 (𝜑 → (𝜓𝜒))
1615sbimdv 2083 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
1716ancld 554 . . . . . . . 8 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1814, 17impbid 215 . . . . . . 7 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
1911, 18syl5bb 286 . . . . . 6 (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20 df-clab 2777 . . . . . 6 (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21 df-clab 2777 . . . . . 6 (𝑧 ∈ {𝑥𝜓} ↔ [𝑧 / 𝑥]𝜓)
2219, 20, 213bitr4g 317 . . . . 5 (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥𝜓}))
2322eqrdv 2796 . . . 4 (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥𝜓})
247, 23syl5eqr 2847 . . 3 (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})} = {𝑥𝜓})
251, 24syl5eq 2845 . 2 (𝜑 → ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
26 df-ss 3898 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
2725, 26sylibr 237 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  [wsb 2069   ∈ wcel 2111  {cab 2776   ∩ cin 3880   ⊆ wss 3881 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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-in 3888  df-ss 3898 This theorem is referenced by:  ss2abi  3994  intss  4860  ssopab2  5399  ssoprab2  7202  suppimacnvss  7826  suppimacnv  7827  ressuppss  7835  ss2ixp  8460  fiss  8875  tcss  9173  tcel  9174  infmap2  9632  cfub  9663  cflm  9664  cflecard  9667  clsslem  14338  cncmet  23936  plyss  24806  iunrnmptss  30339  ofrn2  30411  sigaclci  31516  subfacp1lem6  32560  ss2mcls  32943  itg2addnclem  35127  sdclem1  35200  istotbnd3  35228  sstotbnd  35232  qsss1  35724  aomclem4  40044  hbtlem4  40113  hbtlem3  40114  rngunsnply  40160  iocinico  40205
 Copyright terms: Public domain W3C validator