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

Theorem ss2abdv 4059
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 3954 . . 3 ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
2 df-clab 2710 . . . . . . 7 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
32bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜓𝑦 ∈ {𝑥𝜓})
4 df-clab 2710 . . . . . . 7 (𝑦 ∈ {𝑥𝜒} ↔ [𝑦 / 𝑥]𝜒)
54bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜒𝑦 ∈ {𝑥𝜒})
63, 5anbi12i 627 . . . . 5 (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒}))
76abbii 2802 . . . 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 2710 . . . . . 6 (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21 df-clab 2710 . . . . . 6 (𝑧 ∈ {𝑥𝜓} ↔ [𝑧 / 𝑥]𝜓)
2219, 20, 213bitr4g 313 . . . . 5 (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥𝜓}))
2322eqrdv 2730 . . . 4 (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥𝜓})
247, 23eqtr3id 2786 . . 3 (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})} = {𝑥𝜓})
251, 24eqtrid 2784 . 2 (𝜑 → ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
26 df-ss 3964 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
2725, 26sylibr 233 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  [wsb 2067  wcel 2106  {cab 2709  cin 3946  wss 3947
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 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-in 3954  df-ss 3964
This theorem is referenced by:  ss2abi  4062  abssdv  4064  intss  4972  ssopab2  5545  ssoprab2  7473  suppimacnvss  8154  suppimacnv  8155  ressuppss  8164  ss2ixp  8900  fiss  9415  tcss  9735  tcel  9736  infmap2  10209  cfub  10240  cflm  10241  cflecard  10244  clsslem  14927  cncmet  24830  plyss  25704  iunrnmptss  31784  ofrn2  31852  sigaclci  33118  subfacp1lem6  34164  ss2mcls  34547  itg2addnclem  36527  sdclem1  36599  istotbnd3  36627  sstotbnd  36631  qsss1  37145  disjdmqscossss  37661  sticksstones4  40953  sticksstones14  40964  sticksstones20  40970  sticksstones22  40972  ssabdv  41033  aomclem4  41784  hbtlem4  41853  hbtlem3  41854  rngunsnply  41900  iocinico  41946
  Copyright terms: Public domain W3C validator