Theorem eliun 4938

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
eliun	⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem eliun

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3451	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3135	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2825	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4936	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3624	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3430  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-iun 4936

This theorem is referenced by:  eliuni  4940  eliund  4941  iuncom  4942  iuncom4  4943  iunconst  4944  iuneqconst  4946  iuniin  4947  iinssiun  4948  iunss1  4949  ss2iun  4953  nfiu1  4970  iunssf  4986  iunss  4988  ssiun  4990  ssiun2  4991  iunab  4995  iun0  5005  0iun  5006  iunn0  5010  iunin2  5014  iundif2  5017  iindif2  5020  iunxsng  5033  iunxsngf  5035  iunun  5036  iunxun  5037  iunxdif3  5038  iunxiun  5040  iunpwss  5050  disjiun  5074  disjiund  5077  disjxiun  5083  triun  5208  otiunsndisj  5475  xpiundi  5702  xpiundir  5703  iunxpf  5804  cnvuni  5842  dmiun  5869  dmuni  5870  rniun  6112  xpdifid  6133  dfco2  6210  dfco2a  6211  coiun  6222  imaiun  7200  eluniima  7205  iunpw  7725  fiun  7896  f1iun  7897  opabex3d  7918  opabex3rd  7919  opabex3  7920  onoviun  8283  smoiun  8301  oalimcl  8495  oaass  8496  oarec  8497  omordlim  8512  omlimcl  8513  omeulem1  8517  oelimcl  8536  oeeulem  8537  oaabs2  8585  omabs  8587  dffi3  9344  ixpiunwdom  9505  ttrclselem2  9647  trcl  9649  r1ordg  9702  r1pwss  9708  rankr1ai  9722  r1elss  9730  fseqenlem2  9947  infpwfien  9984  cardaleph  10011  ackbij2  10164  cfsmolem  10192  alephsing  10198  hsmexlem2  10349  ac6c4  10403  ttukeylem6  10436  iunfo  10461  iundom2g  10462  konigthlem  10491  alephreg  10505  pwcfsdom  10506  pwfseqlem3  10583  inar1  10698  inatsk  10701  fsuppmapnn0fiub  13953  wrdval  14478  s3iunsndisj  14930  dfrtrclrec2  15020  fsum2dlem  15732  fsumcom2  15736  fsumiun  15784  fprod2dlem  15945  fprodcom2  15949  prmreclem5  16891  imasaddfnlem  17492  imasvscafn  17501  smndex1basss  18876  smndex1mgm  18878  smndex1mndlem  18880  smndex1n0mnd  18883  efgsfo  19714  frgpnabllem1  19848  lssats2  20995  lbsextlem2  21157  lbsextlem3  21158  islpidl  21323  pzriprnglem10  21470  pzriprnglem12  21472  pzriprnglem13  21473  pzriprnglem14  21474  iunocv  21661  iunconnlem  23392  iunconn  23393  locfincmp  23491  alexsubALTlem3  24014  ptcmplem3  24019  imasdsf1olem  24338  zcld  24779  ovolfioo  25434  ovolficc  25435  ovoliunlem2  25470  ovoliunnul  25474  volfiniun  25514  iundisj  25515  iunmbl2  25524  volsup2  25572  vitalilem2  25576  ismbf3d  25621  mbfaddlem  25627  mbfsup  25631  i1faddlem  25660  i1fmullem  25661  elaa  26282  oldlim  27879  precsexlem10  28208  precsexlem11  28209  numedglnl  29213  clwwlknun  30182  fusgreg2wsp  30406  iunin1f  32627  ssiun3  32628  iunpreima  32634  iundisjf  32659  unipreima  32716  aciunf1lem  32735  ofpreima  32738  iundisjfi  32869  fsumiunle  32902  gsumpart  33124  gsumwrd2dccatlem  33138  elirng  33830  irngnzply1  33835  irngnminplynz  33856  constrconj  33889  locfinreflem  33984  esum2dlem  34236  esum2d  34237  esumiun  34238  eulerpartlemgh  34522  dstfrvunirn  34619  reprsuc  34759  reprdifc  34771  bnj1405  34978  bnj916  35075  bnj983  35093  bnj1398  35176  bnj1417  35183  bnj1498  35203  fmlan0  35573  mclsppslem  35765  colinearex  36242  neibastop2lem  36542  weiunlem  36645  ttctr  36675  rdgellim  37692  exrecfnlem  37695  rabiun  37914  iundif1  37915  volsupnfl  37986  istotbnd3  38092  sstotbnd  38096  sstotbnd3  38097  prdstotbnd  38115  cntotbnd  38117  heiborlem3  38134  heibor  38142  pclfinN  40346  pclcmpatN  40347  lcfrvalsnN  41987  lcfrlem5  41992  lcfrlem6  41993  lcfrlem16  42004  lcfrlem27  42015  lcfrlem37  42025  lcfr  42031  mapdrvallem2  42091  grpods  42633  cnviun  44077  imaiun1  44078  coiun1  44079  ss2iundf  44086  eliunov2  44106  iunconnlem2  45361  iunincfi  45524  eliuniin  45529  eliuniin2  45550  eliunid  45577  iindif2f  45590  unirnmap  45637  unirnmapsn  45643  ssmapsn  45645  iunmapsn  45646  iuneqfzuzlem  45764  allbutfi  45822  fsumiunss  46005  fnlimfvre  46102  cnrefiisplem  46257  dvnprodlem1  46374  dvnprodlem2  46375  fourierdlem80  46614  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0iunmpt  46846  iundjiun  46888  meaiininclem  46914  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem3  47025  hspmbllem2  47055  opnvonmbllem2  47061  iunhoiioolem  47103  smfaddlem1  47191  smflimlem2  47200  smfmullem4  47222  smflimmpt  47238  smflimsuplem7  47254  smflimsuplem8  47255  smflimsupmpt  47257  smfliminfmpt  47260  fsupdm  47270  finfdm  47274  fsetsniunop  47491  otiunsndisjX  47721  iccpartiun  47888  stgredgiun  48428  iunord  50145