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

Theorem ss2abdv 4061
Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011.) Avoid ax-8 2109, ax-10 2138, ax-11 2155, ax-12 2172. (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 3956 . . 3 ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
2 df-clab 2711 . . . . . . 7 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
32bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜓𝑦 ∈ {𝑥𝜓})
4 df-clab 2711 . . . . . . 7 (𝑦 ∈ {𝑥𝜒} ↔ [𝑦 / 𝑥]𝜒)
54bicomi 223 . . . . . 6 ([𝑦 / 𝑥]𝜒𝑦 ∈ {𝑥𝜒})
63, 5anbi12i 628 . . . . 5 (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒}))
76abbii 2803 . . . 4 {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})}
8 sbequ 2087 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜓 ↔ [𝑧 / 𝑥]𝜓))
9 sbequ 2087 . . . . . . . . 9 (𝑦 = 𝑧 → ([𝑦 / 𝑥]𝜒 ↔ [𝑧 / 𝑥]𝜒))
108, 9anbi12d 632 . . . . . . . 8 (𝑦 = 𝑧 → (([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1110sbievw 2096 . . . . . . 7 ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒))
12 ax-1 6 . . . . . . . . . 10 ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓))
1312a1i 11 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜒 → [𝑧 / 𝑥]𝜓)))
1413impd 412 . . . . . . . 8 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) → [𝑧 / 𝑥]𝜓))
15 ss2abdv.1 . . . . . . . . . 10 (𝜑 → (𝜓𝜒))
1615sbimdv 2082 . . . . . . . . 9 (𝜑 → ([𝑧 / 𝑥]𝜓 → [𝑧 / 𝑥]𝜒))
1716ancld 552 . . . . . . . 8 (𝜑 → ([𝑧 / 𝑥]𝜓 → ([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒)))
1814, 17impbid 211 . . . . . . 7 (𝜑 → (([𝑧 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
1911, 18bitrid 283 . . . . . 6 (𝜑 → ([𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒) ↔ [𝑧 / 𝑥]𝜓))
20 df-clab 2711 . . . . . 6 (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ [𝑧 / 𝑦]([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
21 df-clab 2711 . . . . . 6 (𝑧 ∈ {𝑥𝜓} ↔ [𝑧 / 𝑥]𝜓)
2219, 20, 213bitr4g 314 . . . . 5 (𝜑 → (𝑧 ∈ {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} ↔ 𝑧 ∈ {𝑥𝜓}))
2322eqrdv 2731 . . . 4 (𝜑 → {𝑦 ∣ ([𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒)} = {𝑥𝜓})
247, 23eqtr3id 2787 . . 3 (𝜑 → {𝑦 ∣ (𝑦 ∈ {𝑥𝜓} ∧ 𝑦 ∈ {𝑥𝜒})} = {𝑥𝜓})
251, 24eqtrid 2785 . 2 (𝜑 → ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
26 df-ss 3966 . 2 ({𝑥𝜓} ⊆ {𝑥𝜒} ↔ ({𝑥𝜓} ∩ {𝑥𝜒}) = {𝑥𝜓})
2725, 26sylibr 233 1 (𝜑 → {𝑥𝜓} ⊆ {𝑥𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  [wsb 2068  wcel 2107  {cab 2710  cin 3948  wss 3949
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-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-in 3956  df-ss 3966
This theorem is referenced by:  ss2abi  4064  abssdv  4066  intss  4974  ssopab2  5547  ssoprab2  7477  suppimacnvss  8158  suppimacnv  8159  ressuppss  8168  ss2ixp  8904  fiss  9419  tcss  9739  tcel  9740  infmap2  10213  cfub  10244  cflm  10245  cflecard  10248  clsslem  14931  cncmet  24839  plyss  25713  iunrnmptss  31797  ofrn2  31865  sigaclci  33130  subfacp1lem6  34176  ss2mcls  34559  itg2addnclem  36539  sdclem1  36611  istotbnd3  36639  sstotbnd  36643  qsss1  37157  disjdmqscossss  37673  sticksstones4  40965  sticksstones14  40976  sticksstones20  40982  sticksstones22  40984  ssabdv  41037  aomclem4  41799  hbtlem4  41868  hbtlem3  41869  rngunsnply  41915  iocinico  41961
  Copyright terms: Public domain W3C validator