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

Theorem eliun 3717
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem eliun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elex 2624 . 2  |-  ( A  e.  U_ x  e.  B  C  ->  A  e.  _V )
2 elex 2624 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32rexlimivw 2481 . 2  |-  ( E. x  e.  B  A  e.  C  ->  A  e. 
_V )
4 eleq1 2147 . . . 4  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
54rexbidv 2377 . . 3  |-  ( y  =  A  ->  ( E. x  e.  B  y  e.  C  <->  E. x  e.  B  A  e.  C ) )
6 df-iun 3715 . . 3  |-  U_ x  e.  B  C  =  { y  |  E. x  e.  B  y  e.  C }
75, 6elab2g 2753 . 2  |-  ( A  e.  _V  ->  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C ) )
81, 3, 7pm5.21nii 653 1  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 103    = wceq 1287    e. wcel 1436   E.wrex 2356   _Vcvv 2615   U_ciun 3713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2617  df-iun 3715
This theorem is referenced by:  iuncom  3719  iuncom4  3720  iunconstm  3721  iuniin  3723  iunss1  3724  ss2iun  3728  dfiun2g  3745  ssiun  3755  ssiun2  3756  iunab  3759  iun0  3769  0iun  3770  iunn0m  3773  iunin2  3776  iundif2ss  3778  iindif2m  3780  iunxsng  3788  iunun  3790  iunxun  3791  iunxiun  3792  iunpwss  3799  triun  3924  iunpw  4275  xpiundi  4464  xpiundir  4465  iunxpf  4552  cnvuni  4590  dmiun  4613  dmuni  4614  rniun  4808  dfco2  4896  dfco2a  4897  coiun  4906  fun11iun  5237  imaiun  5500  eluniimadm  5505  opabex3d  5849  opabex3  5850  smoiun  6020  tfrlemi14d  6052  tfr1onlemres  6068  tfrcllemres  6081
  Copyright terms: Public domain W3C validator