Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssundif Structured version   Unicode version

Theorem ssundif 3735
 Description: A condition equivalent to inclusion in the union of two classes. (Contributed by NM, 26-Mar-2007.)
Assertion
Ref Expression
ssundif

Proof of Theorem ssundif
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 pm5.6 880 . . . 4
2 eldif 3316 . . . . 5
32imbi1i 317 . . . 4
4 elun 3474 . . . . 5
54imbi2i 305 . . . 4
61, 3, 53bitr4ri 271 . . 3
76albii 1576 . 2
8 dfss2 3323 . 2
9 dfss2 3323 . 2
107, 8, 93bitr4i 270 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wo 359   wa 360  wal 1550   wcel 1727   cdif 3303   cun 3304   wss 3306 This theorem is referenced by:  difcom  3736  uneqdifeq  3740  ssunsn2  3982  elpwun  4785  soex  5348  frfi  7381  cantnfp1lem3  7665  dfacfin7  8310  zornn0g  8416  fpwwe2lem13  8548  hashbclem  11732  incexclem  12647  ramub1lem1  13425  lpcls  17459  cmpcld  17496  alexsubALTlem3  18111  restmetu  18648  uniiccdif  19501  abelthlem2  20379  abelthlem3  20380 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320
 Copyright terms: Public domain W3C validator