MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunss Structured version   Visualization version   GIF version

Theorem iunss 4945
Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
iunss ( 𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵𝐶)
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iunss
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-iun 4897 . . 3 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
21sseq1i 3974 . 2 ( 𝑥𝐴 𝐵𝐶 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶)
3 abss 4019 . 2 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
4 dfss2 3933 . . . 4 (𝐵𝐶 ↔ ∀𝑦(𝑦𝐵𝑦𝐶))
54ralbii 3152 . . 3 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶))
6 ralcom4 3222 . . 3 (∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶))
7 r19.23v 3266 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ (∃𝑥𝐴 𝑦𝐵𝑦𝐶))
87albii 1820 . . 3 (∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
95, 6, 83bitrri 300 . 2 (∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶) ↔ ∀𝑥𝐴 𝐵𝐶)
102, 3, 93bitri 299 1 ( 𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wal 1535  wcel 2114  {cab 2798  wral 3125  wrex 3126  wss 3913   ciun 4895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rex 3131  df-v 3475  df-in 3920  df-ss 3930  df-iun 4897
This theorem is referenced by:  iunss2  4949  iunssd  4950  djussxp  5692  fiun  7622  f1iun  7623  wfrdmss  7939  onfununi  7956  oawordeulem  8158  oaabslem  8248  oaabs2  8250  omabslem  8251  omabs  8252  marypha2lem1  8877  trcl  9148  r1val1  9193  rankuni2b  9260  rankval4  9274  rankbnd  9275  rankbnd2  9276  rankc1  9277  cfslb2n  9668  cfsmolem  9670  hsmexlem2  9827  axdc3lem2  9851  ac6  9880  wuncval2  10147  inar1  10175  tskuni  10183  grur1a  10219  fsuppmapnn0fiublem  13342  fsuppmapnn0fiub  13343  rtrclreclem4  14400  prmreclem4  16233  prmreclem5  16234  prdsval  16707  prdsbas  16709  imasaddfnlem  16780  imasvscafn  16789  imasvscaf  16791  isacs2  16903  mreacs  16908  acsfn  16909  dmcoass  17305  isacs5  17761  dprdspan  19128  dprd2dlem1  19142  dprd2d2  19145  dmdprdsplit2lem  19146  lbsextlem2  19907  lpival  19994  iunocv  20801  tgidm  21564  iunconn  22012  comppfsc  22116  txtube  22224  txcmplem2  22226  xkococnlem  22243  xkoinjcn  22271  alexsubALTlem3  22633  cnextf  22650  imasdsf1olem  22959  metnrmlem3  23445  ovolfiniun  24084  ovoliunlem2  24086  ovoliun  24088  ovoliunnul  24090  volfiniun  24130  voliunlem1  24133  volsup  24139  uniioombllem3a  24167  uniioombllem3  24168  uniioombllem4  24169  ismbf3d  24237  limciun  24476  taylfval  24933  taylf  24935  elpwiuncl  30275  disjunsn  30331  esum2d  31360  omssubadd  31566  eulerpartlemgh  31644  eulerpartlemgs2  31646  bnj226  32012  bnj517  32165  bnj1118  32264  bnj1137  32275  cvmlift2lem12  32569  trpredlem1  33074  trpredss  33076  trpredmintr  33078  dftrpred3g  33080  frrlem7  33137  ntruni  33683  neibastop2lem  33716  filnetlem4  33737  mblfinlem2  34971  volsupnfl  34978  cnambfre  34981  sstotbnd2  35088  equivtotbnd  35092  totbndbnd  35103  prdstotbnd  35108  heiborlem1  35125  pclfinN  37072  lcfrlem4  38717  lcfrlem16  38730  lcfr  38757  iunrelexp0  40182  iunrelexpmin1  40188  iunrelexpmin2  40192  cotrcltrcl  40205  trclimalb2  40206  cotrclrcl  40222  iunconnlem2  41424  ixpssmapc  41491  ioorrnopnlem  42737  omeiunle  42947  omeiunltfirp  42949  carageniuncl  42953  caratheodorylem1  42956  caratheodorylem2  42957  hoissrrn  42979  ovnlecvr  42988  ovnsubaddlem1  43000  ovnsubadd  43002  hoissrrn2  43008  ovnlecvr2  43040  hspmbl  43059  opnvonmbllem2  43063  vonvolmbllem  43090  vonvolmbl2  43093  vonvol2  43094  iunhoiioolem  43105  iunhoiioo  43106
  Copyright terms: Public domain W3C validator