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

Theorem eliun 3651
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun (A x B 𝐶x B A 𝐶)
Distinct variable group:   x,A
Allowed substitution hints:   B(x)   𝐶(x)

Proof of Theorem eliun
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 elex 2560 . 2 (A x B 𝐶A V)
2 elex 2560 . . 3 (A 𝐶A V)
32rexlimivw 2423 . 2 (x B A 𝐶A V)
4 eleq1 2097 . . . 4 (y = A → (y 𝐶A 𝐶))
54rexbidv 2321 . . 3 (y = A → (x B y 𝐶x B A 𝐶))
6 df-iun 3649 . . 3 x B 𝐶 = {yx B y 𝐶}
75, 6elab2g 2683 . 2 (A V → (A x B 𝐶x B A 𝐶))
81, 3, 7pm5.21nii 619 1 (A x B 𝐶x B A 𝐶)
Colors of variables: wff set class
Syntax hints:  wb 98   = wceq 1242   wcel 1390  wrex 2301  Vcvv 2551   ciun 3647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-iun 3649
This theorem is referenced by:  iuncom  3653  iuncom4  3654  iunconstm  3655  iuniin  3657  iunss1  3658  ss2iun  3662  dfiun2g  3679  ssiun  3689  ssiun2  3690  iunab  3693  iun0  3703  0iun  3704  iunn0m  3707  iunin2  3710  iundif2ss  3712  iindif2m  3714  iunxsng  3722  iunun  3724  iunxun  3725  iunxiun  3726  iunpwss  3733  triun  3857  iunpw  4176  xpiundi  4340  xpiundir  4341  iunxpf  4426  cnvuni  4463  dmiun  4486  dmuni  4487  rniun  4676  dfco2  4762  dfco2a  4763  coiun  4772  fun11iun  5088  imaiun  5340  eluniimadm  5345  opabex3d  5687  opabex3  5688  smoiun  5854  tfrlemi14d  5885
  Copyright terms: Public domain W3C validator