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

Theorem reldisj 3873
Description: Two ways of saying that two classes are disjoint, using the complement of  B relative to a universe  C. (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
reldisj  |-  ( A 
C_  C  ->  (
( A  i^i  B
)  =  (/)  <->  A  C_  ( C  \  B ) ) )

Proof of Theorem reldisj
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfss2 3488 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
2 pm5.44 911 . . . . . 6  |-  ( ( x  e.  A  ->  x  e.  C )  ->  ( ( x  e.  A  ->  -.  x  e.  B )  <->  ( x  e.  A  ->  ( x  e.  C  /\  -.  x  e.  B )
) ) )
3 eldif 3481 . . . . . . 7  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
43imbi2i 312 . . . . . 6  |-  ( ( x  e.  A  ->  x  e.  ( C  \  B ) )  <->  ( x  e.  A  ->  ( x  e.  C  /\  -.  x  e.  B )
) )
52, 4syl6bbr 263 . . . . 5  |-  ( ( x  e.  A  ->  x  e.  C )  ->  ( ( x  e.  A  ->  -.  x  e.  B )  <->  ( x  e.  A  ->  x  e.  ( C  \  B
) ) ) )
65sps 1866 . . . 4  |-  ( A. x ( x  e.  A  ->  x  e.  C )  ->  (
( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  ->  x  e.  ( C  \  B ) ) ) )
71, 6sylbi 195 . . 3  |-  ( A 
C_  C  ->  (
( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  ->  x  e.  ( C  \  B ) ) ) )
87albidv 1714 . 2  |-  ( A 
C_  C  ->  ( A. x ( x  e.  A  ->  -.  x  e.  B )  <->  A. x
( x  e.  A  ->  x  e.  ( C 
\  B ) ) ) )
9 disj1 3872 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
10 dfss2 3488 . 2  |-  ( A 
C_  ( C  \  B )  <->  A. x
( x  e.  A  ->  x  e.  ( C 
\  B ) ) )
118, 9, 103bitr4g 288 1  |-  ( A 
C_  C  ->  (
( A  i^i  B
)  =  (/)  <->  A  C_  ( C  \  B ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1393    = wceq 1395    e. wcel 1819    \ cdif 3468    i^i cin 3470    C_ wss 3471   (/)c0 3793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794
This theorem is referenced by:  disj2  3877  oacomf1olem  7231  domdifsn  7619  elfiun  7908  cantnfp1lem3  8116  cantnfp1lem3OLD  8142  ssxr  9671  structcnvcnv  14655  fidomndrng  18083  elcls  19701  ist1-2  19975  nrmsep2  19984  nrmsep  19985  isnrm3  19987  isreg2  20005  hauscmplem  20033  connsub  20048  iunconlem  20054  llycmpkgen2  20177  hausdiag  20272  trfil3  20515  isufil2  20535  filufint  20547  blcld  21134  i1fima2  22212  i1fd  22214  usgrares1  24537  nbgrassvwo  24564  nbgrassvwo2  24565  itg2addnclem2  30251
  Copyright terms: Public domain W3C validator