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

Theorem iunss 4488
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 4448 . . 3 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
21sseq1i 3588 . 2 ( 𝑥𝐴 𝐵𝐶 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶)
3 abss 3630 . 2 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
4 dfss2 3553 . . . 4 (𝐵𝐶 ↔ ∀𝑦(𝑦𝐵𝑦𝐶))
54ralbii 2959 . . 3 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶))
6 ralcom4 3193 . . 3 (∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶))
7 r19.23v 3001 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ (∃𝑥𝐴 𝑦𝐵𝑦𝐶))
87albii 1736 . . 3 (∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
95, 6, 83bitrri 285 . 2 (∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶) ↔ ∀𝑥𝐴 𝐵𝐶)
102, 3, 93bitri 284 1 ( 𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wal 1472  wcel 1976  {cab 2592  wral 2892  wrex 2893  wss 3536   ciun 4446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-v 3171  df-in 3543  df-ss 3550  df-iun 4448
This theorem is referenced by:  iunss2  4492  djussxp  5174  fun11iun  6993  wfrdmss  7282  onfununi  7299  oawordeulem  7495  oaabslem  7584  oaabs2  7586  omabslem  7587  omabs  7588  marypha2lem1  8198  trcl  8461  r1val1  8506  rankuni2b  8573  rankval4  8587  rankbnd  8588  rankbnd2  8589  rankc1  8590  cfslb2n  8947  cfsmolem  8949  hsmexlem2  9106  axdc3lem2  9130  ac6  9159  wuncval2  9422  inar1  9450  tskuni  9458  grur1a  9494  fsuppmapnn0fiublem  12603  fsuppmapnn0fiub  12604  fsuppmapnn0fiubOLD  12605  wrdexg  13113  rtrclreclem4  13592  prmreclem4  15404  prmreclem5  15405  prdsval  15881  prdsbas  15883  imasaddfnlem  15954  imasaddflem  15956  imasvscafn  15963  imasvscaf  15965  isacs2  16080  mreacs  16085  acsfn  16086  dmcoass  16482  isacs5  16938  dprdspan  18192  dprd2dlem1  18206  dprd2d2  18209  dmdprdsplit2lem  18210  lbsextlem2  18923  lpival  19009  iunocv  19783  tgidm  20534  iuncon  20980  comppfsc  21084  txtube  21192  txcmplem2  21194  xkococnlem  21211  xkoinjcn  21239  alexsubALTlem3  21602  cnextf  21619  imasdsf1olem  21926  metnrmlem3  22400  ovolfiniun  22990  ovoliunlem2  22992  ovoliun  22994  ovoliunnul  22996  volfiniun  23036  voliunlem1  23039  volsup  23045  uniioombllem3a  23072  uniioombllem3  23073  uniioombllem4  23074  ismbf3d  23141  limciun  23378  taylfval  23831  taylf  23833  elpwiuncl  28546  disjunsn  28592  esum2d  29285  omssubadd  29492  eulerpartlemgh  29570  eulerpartlemgs2  29572  bnj226  29859  bnj517  30012  bnj1118  30109  bnj1137  30120  cvmlift2lem12  30353  trpredlem1  30774  trpredss  30776  trpredmintr  30778  dftrpred3g  30780  frrlem5d  30834  frrlem7  30837  nofulllem5  30908  ntruni  31295  neibastop2lem  31328  filnetlem4  31349  mblfinlem2  32417  volsupnfl  32424  cnambfre  32428  sstotbnd2  32543  equivtotbnd  32547  totbndbnd  32558  prdstotbnd  32563  heiborlem1  32580  pclfinN  34004  lcfrlem4  35652  lcfrlem16  35665  lcfr  35692  iunrelexp0  36813  iunrelexpmin1  36819  iunrelexpmin2  36823  cotrcltrcl  36836  trclimalb2  36837  cotrclrcl  36853  iunconlem2  37993  ixpssmapc  38069  iunssd  38099  ioorrnopnlem  39001  omeiunle  39208  omeiunltfirp  39210  carageniuncl  39214  caratheodorylem1  39217  caratheodorylem2  39218  hoissrrn  39240  ovnlecvr  39249  ovnsubaddlem1  39261  ovnsubadd  39263  hoissrrn2  39269  ovnlecvr2  39301  hspmbl  39320  opnvonmbllem2  39324  vonvolmbllem  39351  vonvolmbl2  39354  vonvol2  39355  iunhoiioolem  39367  iunhoiioo  39368
  Copyright terms: Public domain W3C validator