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

Theorem ss2rab 3662
Description: Restricted abstraction classes in a subclass relationship. (Contributed by NM, 30-May-1999.)
Assertion
Ref Expression
ss2rab ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))

Proof of Theorem ss2rab
StepHypRef Expression
1 df-rab 2916 . . 3 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
2 df-rab 2916 . . 3 {𝑥𝐴𝜓} = {𝑥 ∣ (𝑥𝐴𝜓)}
31, 2sseq12i 3615 . 2 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ {𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐴𝜓)})
4 ss2ab 3654 . 2 ({𝑥 ∣ (𝑥𝐴𝜑)} ⊆ {𝑥 ∣ (𝑥𝐴𝜓)} ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐴𝜓)))
5 df-ral 2912 . . 3 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥(𝑥𝐴 → (𝜑𝜓)))
6 imdistan 724 . . . 4 ((𝑥𝐴 → (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) → (𝑥𝐴𝜓)))
76albii 1744 . . 3 (∀𝑥(𝑥𝐴 → (𝜑𝜓)) ↔ ∀𝑥((𝑥𝐴𝜑) → (𝑥𝐴𝜓)))
85, 7bitr2i 265 . 2 (∀𝑥((𝑥𝐴𝜑) → (𝑥𝐴𝜓)) ↔ ∀𝑥𝐴 (𝜑𝜓))
93, 4, 83bitri 286 1 ({𝑥𝐴𝜑} ⊆ {𝑥𝐴𝜓} ↔ ∀𝑥𝐴 (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478  wcel 1987  {cab 2607  wral 2907  {crab 2911  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rab 2916  df-in 3566  df-ss 3573
This theorem is referenced by:  ss2rabdv  3667  ss2rabi  3668  mptexgf  6445  scottex  8700  ondomon  9337  eltsms  21859  xrlimcnp  24612  wwlksnfi  26687  disjxwwlkn  26694  occon  28016  spanss  28077  chpssati  29092  lpssat  33815  lssatle  33817  lssat  33818  atlatle  34122  pmaple  34562  diaord  35851  mapdordlem2  36441  rmxyelqirr  36990  itgoss  37249  ovnsslelem  40107  ovolval5lem3  40201  pimiooltgt  40254  preimageiingt  40263  preimaleiinlt  40264
  Copyright terms: Public domain W3C validator