ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnvuni Unicode version

Theorem cnvuni 4772
Description: The converse of a class union is the (indexed) union of the converses of its members. (Contributed by NM, 11-Aug-2004.)
Assertion
Ref Expression
cnvuni  |-  `' U. A  =  U_ x  e.  A  `' x
Distinct variable group:    x, A

Proof of Theorem cnvuni
Dummy variables  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elcnv2 4764 . . . 4  |-  ( y  e.  `' U. A  <->  E. z E. w ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  U. A ) )
2 eluni2 3776 . . . . . . 7  |-  ( <.
w ,  z >.  e.  U. A  <->  E. x  e.  A  <. w ,  z >.  e.  x
)
32anbi2i 453 . . . . . 6  |-  ( ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  U. A )  <->  ( y  =  <. z ,  w >.  /\  E. x  e.  A  <. w ,  z
>.  e.  x ) )
4 r19.42v 2614 . . . . . 6  |-  ( E. x  e.  A  ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  x
)  <->  ( y  = 
<. z ,  w >.  /\ 
E. x  e.  A  <. w ,  z >.  e.  x ) )
53, 4bitr4i 186 . . . . 5  |-  ( ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  U. A )  <->  E. x  e.  A  ( y  =  <. z ,  w >.  /\  <. w ,  z
>.  e.  x ) )
652exbii 1586 . . . 4  |-  ( E. z E. w ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  U. A )  <->  E. z E. w E. x  e.  A  ( y  = 
<. z ,  w >.  /\ 
<. w ,  z >.  e.  x ) )
7 elcnv2 4764 . . . . . 6  |-  ( y  e.  `' x  <->  E. z E. w ( y  = 
<. z ,  w >.  /\ 
<. w ,  z >.  e.  x ) )
87rexbii 2464 . . . . 5  |-  ( E. x  e.  A  y  e.  `' x  <->  E. x  e.  A  E. z E. w ( y  = 
<. z ,  w >.  /\ 
<. w ,  z >.  e.  x ) )
9 rexcom4 2735 . . . . 5  |-  ( E. x  e.  A  E. z E. w ( y  =  <. z ,  w >.  /\  <. w ,  z
>.  e.  x )  <->  E. z E. x  e.  A  E. w ( y  = 
<. z ,  w >.  /\ 
<. w ,  z >.  e.  x ) )
10 rexcom4 2735 . . . . . 6  |-  ( E. x  e.  A  E. w ( y  = 
<. z ,  w >.  /\ 
<. w ,  z >.  e.  x )  <->  E. w E. x  e.  A  ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  x
) )
1110exbii 1585 . . . . 5  |-  ( E. z E. x  e.  A  E. w ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  x
)  <->  E. z E. w E. x  e.  A  ( y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  x
) )
128, 9, 113bitrri 206 . . . 4  |-  ( E. z E. w E. x  e.  A  (
y  =  <. z ,  w >.  /\  <. w ,  z >.  e.  x
)  <->  E. x  e.  A  y  e.  `' x
)
131, 6, 123bitri 205 . . 3  |-  ( y  e.  `' U. A  <->  E. x  e.  A  y  e.  `' x )
14 eliun 3853 . . 3  |-  ( y  e.  U_ x  e.  A  `' x  <->  E. x  e.  A  y  e.  `' x )
1513, 14bitr4i 186 . 2  |-  ( y  e.  `' U. A  <->  y  e.  U_ x  e.  A  `' x )
1615eqriv 2154 1  |-  `' U. A  =  U_ x  e.  A  `' x
Colors of variables: wff set class
Syntax hints:    /\ wa 103    = wceq 1335   E.wex 1472    e. wcel 2128   E.wrex 2436   <.cop 3563   U.cuni 3772   U_ciun 3849   `'ccnv 4585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-iun 3851  df-br 3966  df-opab 4026  df-cnv 4594
This theorem is referenced by:  funcnvuni  5239
  Copyright terms: Public domain W3C validator