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

Theorem reldisj 3838
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 3453 . . . 4  |-  ( A 
C_  C  <->  A. x
( x  e.  A  ->  x  e.  C ) )
2 pm5.44 919 . . . . . 6  |-  ( ( x  e.  A  ->  x  e.  C )  ->  ( ( x  e.  A  ->  -.  x  e.  B )  <->  ( x  e.  A  ->  ( x  e.  C  /\  -.  x  e.  B )
) ) )
3 eldif 3446 . . . . . . 7  |-  ( x  e.  ( C  \  B )  <->  ( x  e.  C  /\  -.  x  e.  B ) )
43imbi2i 313 . . . . . 6  |-  ( ( x  e.  A  ->  x  e.  ( C  \  B ) )  <->  ( x  e.  A  ->  ( x  e.  C  /\  -.  x  e.  B )
) )
52, 4syl6bbr 266 . . . . 5  |-  ( ( x  e.  A  ->  x  e.  C )  ->  ( ( x  e.  A  ->  -.  x  e.  B )  <->  ( x  e.  A  ->  x  e.  ( C  \  B
) ) ) )
65sps 1920 . . . 4  |-  ( A. x ( x  e.  A  ->  x  e.  C )  ->  (
( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  ->  x  e.  ( C  \  B ) ) ) )
71, 6sylbi 198 . . 3  |-  ( A 
C_  C  ->  (
( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  ->  x  e.  ( C  \  B ) ) ) )
87albidv 1761 . 2  |-  ( A 
C_  C  ->  ( A. x ( x  e.  A  ->  -.  x  e.  B )  <->  A. x
( x  e.  A  ->  x  e.  ( C 
\  B ) ) ) )
9 disj1 3837 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
10 dfss2 3453 . 2  |-  ( A 
C_  ( C  \  B )  <->  A. x
( x  e.  A  ->  x  e.  ( C 
\  B ) ) )
118, 9, 103bitr4g 291 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 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1872    \ cdif 3433    i^i cin 3435    C_ wss 3436   (/)c0 3761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-v 3082  df-dif 3439  df-in 3443  df-ss 3450  df-nul 3762
This theorem is referenced by:  disj2  3842  oacomf1olem  7276  domdifsn  7664  elfiun  7953  cantnfp1lem3  8193  ssxr  9710  structcnvcnv  15131  fidomndrng  18530  elcls  20087  ist1-2  20361  nrmsep2  20370  nrmsep  20371  isnrm3  20373  isreg2  20391  hauscmplem  20419  connsub  20434  iunconlem  20440  llycmpkgen2  20563  hausdiag  20658  trfil3  20901  isufil2  20921  filufint  20933  blcld  21518  i1fima2  22635  i1fd  22637  usgrares1  25136  nbgrassvwo  25163  nbgrassvwo2  25164  poimirlem15  31919  itg2addnclem2  31958  nbgrssvwo2  39198
  Copyright terms: Public domain W3C validator