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

Theorem ss2abdv 4018
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2108, ax-10 2137, ax-11 2154, ax-12 2171. (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 3915 . . 3 ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
2 df-clab 2714 . . . . . . 7 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
32bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜓𝑦 ∈ {𝑥𝜓})
4 df-clab 2714 . . . . . . 7 (𝑦 ∈ {𝑥𝜒} ↔ [𝑦 / 𝑥]𝜒)
54bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜒𝑦 ∈ {𝑥𝜒})
63, 5anbi12i 627 . . . . 5 (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒}))
76abbii 2806 . . . 4 {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
8 sbequ 2086 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9 sbequ 2086 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
108, 9anbi12d 631 . . . . . . . 8 (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1110sbievw 2095 . . . . . . 7 ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12 ax-1 6 . . . . . . . . . 10 ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
1312a1i 11 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
1413impd 411 . . . . . . . 8 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15 ss2abdv.1 . . . . . . . . . 10 (𝜑 → (𝜓𝜒))
1615sbimdv 2081 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
1716ancld 551 . . . . . . . 8 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1814, 17impbid 211 . . . . . . 7 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
1911, 18bitrid 282 . . . . . 6 (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20 df-clab 2714 . . . . . 6 (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21 df-clab 2714 . . . . . 6 (𝑧 ∈ {𝑥𝜓} ↔ [𝑧 / 𝑥]𝜓)
2219, 20, 213bitr4g 313 . . . . 5 (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥𝜓}))
2322eqrdv 2734 . . . 4 (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥𝜓})
247, 23eqtr3id 2790 . . 3 (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})} = {𝑥𝜓})
251, 24eqtrid 2788 . 2 (𝜑 → ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
26 df-ss 3925 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
2725, 26sylibr 233 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  [wsb 2067  wcel 2106  {cab 2713  cin 3907  wss 3908
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-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-in 3915  df-ss 3925
This theorem is referenced by:  ss2abi  4021  abssdv  4023  intss  4928  ssopab2  5501  ssoprab2  7419  suppimacnvss  8096  suppimacnv  8097  ressuppss  8106  ss2ixp  8806  fiss  9318  tcss  9638  tcel  9639  infmap2  10112  cfub  10143  cflm  10144  cflecard  10147  clsslem  14823  cncmet  24632  plyss  25506  iunrnmptss  31329  ofrn2  31401  sigaclci  32559  subfacp1lem6  33607  ss2mcls  33990  itg2addnclem  36061  sdclem1  36134  istotbnd3  36162  sstotbnd  36166  qsss1  36681  disjdmqscossss  37197  sticksstones4  40489  sticksstones14  40500  sticksstones20  40506  sticksstones22  40508  ssabdv  40573  aomclem4  41287  hbtlem4  41356  hbtlem3  41357  rngunsnply  41403  iocinico  41449
  Copyright terms: Public domain W3C validator