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

Theorem iunss 4593
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 4554 . . 3 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
21sseq1i 3662 . 2 ( 𝑥𝐴 𝐵𝐶 ↔ {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶)
3 abss 3704 . 2 ({𝑦 ∣ ∃𝑥𝐴 𝑦𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
4 dfss2 3624 . . . 4 (𝐵𝐶 ↔ ∀𝑦(𝑦𝐵𝑦𝐶))
54ralbii 3009 . . 3 (∀𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶))
6 ralcom4 3255 . . 3 (∀𝑥𝐴𝑦(𝑦𝐵𝑦𝐶) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶))
7 r19.23v 3052 . . . 4 (∀𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ (∃𝑥𝐴 𝑦𝐵𝑦𝐶))
87albii 1787 . . 3 (∀𝑦𝑥𝐴 (𝑦𝐵𝑦𝐶) ↔ ∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶))
95, 6, 83bitrri 287 . 2 (∀𝑦(∃𝑥𝐴 𝑦𝐵𝑦𝐶) ↔ ∀𝑥𝐴 𝐵𝐶)
102, 3, 93bitri 286 1 ( 𝑥𝐴 𝐵𝐶 ↔ ∀𝑥𝐴 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wal 1521  wcel 2030  {cab 2637  wral 2941  wrex 2942  wss 3607   ciun 4552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-in 3614  df-ss 3621  df-iun 4554
This theorem is referenced by:  iunss2  4597  djussxp  5300  fun11iun  7168  wfrdmss  7466  onfununi  7483  oawordeulem  7679  oaabslem  7768  oaabs2  7770  omabslem  7771  omabs  7772  marypha2lem1  8382  trcl  8642  r1val1  8687  rankuni2b  8754  rankval4  8768  rankbnd  8769  rankbnd2  8770  rankc1  8771  cfslb2n  9128  cfsmolem  9130  hsmexlem2  9287  axdc3lem2  9311  ac6  9340  wuncval2  9607  inar1  9635  tskuni  9643  grur1a  9679  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  wrdexg  13347  rtrclreclem4  13845  prmreclem4  15670  prmreclem5  15671  prdsval  16162  prdsbas  16164  imasaddfnlem  16235  imasaddflem  16237  imasvscafn  16244  imasvscaf  16246  isacs2  16361  mreacs  16366  acsfn  16367  dmcoass  16763  isacs5  17219  dprdspan  18472  dprd2dlem1  18486  dprd2d2  18489  dmdprdsplit2lem  18490  lbsextlem2  19207  lpival  19293  iunocv  20073  tgidm  20832  iunconn  21279  comppfsc  21383  txtube  21491  txcmplem2  21493  xkococnlem  21510  xkoinjcn  21538  alexsubALTlem3  21900  cnextf  21917  imasdsf1olem  22225  metnrmlem3  22711  ovolfiniun  23315  ovoliunlem2  23317  ovoliun  23319  ovoliunnul  23321  volfiniun  23361  voliunlem1  23364  volsup  23370  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  ismbf3d  23466  limciun  23703  taylfval  24158  taylf  24160  elpwiuncl  29485  disjunsn  29533  esum2d  30283  omssubadd  30490  eulerpartlemgh  30568  eulerpartlemgs2  30570  bnj226  30928  bnj517  31081  bnj1118  31178  bnj1137  31189  cvmlift2lem12  31422  trpredlem1  31851  trpredss  31853  trpredmintr  31855  dftrpred3g  31857  frrlem5d  31912  frrlem7  31915  ntruni  32447  neibastop2lem  32480  filnetlem4  32501  mblfinlem2  33577  volsupnfl  33584  cnambfre  33588  sstotbnd2  33703  equivtotbnd  33707  totbndbnd  33718  prdstotbnd  33723  heiborlem1  33740  pclfinN  35504  lcfrlem4  37151  lcfrlem16  37164  lcfr  37191  iunrelexp0  38311  iunrelexpmin1  38317  iunrelexpmin2  38321  cotrcltrcl  38334  trclimalb2  38335  cotrclrcl  38351  iunconnlem2  39485  ixpssmapc  39557  iunssd  39585  ioorrnopnlem  40842  omeiunle  41052  omeiunltfirp  41054  carageniuncl  41058  caratheodorylem1  41061  caratheodorylem2  41062  hoissrrn  41084  ovnlecvr  41093  ovnsubaddlem1  41105  ovnsubadd  41107  hoissrrn2  41113  ovnlecvr2  41145  hspmbl  41164  opnvonmbllem2  41168  vonvolmbllem  41195  vonvolmbl2  41198  vonvol2  41199  iunhoiioolem  41210  iunhoiioo  41211
  Copyright terms: Public domain W3C validator