Theorem iunss 4497

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.

Step	Hyp	Ref	Expression
1		df-iun 4457	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3592	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3634	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3557	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 2963	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3197	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3005	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1737	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 286	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 285	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 195  ∀wal 1473   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-iun 4457

This theorem is referenced by:  iunss2  4501  djussxp  5189  fun11iun  7019  wfrdmss  7308  onfununi  7325  oawordeulem  7521  oaabslem  7610  oaabs2  7612  omabslem  7613  omabs  7614  marypha2lem1  8224  trcl  8487  r1val1  8532  rankuni2b  8599  rankval4  8613  rankbnd  8614  rankbnd2  8615  rankc1  8616  cfslb2n  8973  cfsmolem  8975  hsmexlem2  9132  axdc3lem2  9156  ac6  9185  wuncval2  9448  inar1  9476  tskuni  9484  grur1a  9520  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  wrdexg  13170  rtrclreclem4  13649  prmreclem4  15461  prmreclem5  15462  prdsval  15938  prdsbas  15940  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasvscaf  16022  isacs2  16137  mreacs  16142  acsfn  16143  dmcoass  16539  isacs5  16995  dprdspan  18249  dprd2dlem1  18263  dprd2d2  18266  dmdprdsplit2lem  18267  lbsextlem2  18980  lpival  19066  iunocv  19844  tgidm  20595  iuncon  21041  comppfsc  21145  txtube  21253  txcmplem2  21255  xkococnlem  21272  xkoinjcn  21300  alexsubALTlem3  21663  cnextf  21680  imasdsf1olem  21988  metnrmlem3  22472  ovolfiniun  23076  ovoliunlem2  23078  ovoliun  23080  ovoliunnul  23082  volfiniun  23122  voliunlem1  23125  volsup  23131  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  ismbf3d  23227  limciun  23464  taylfval  23917  taylf  23919  elpwiuncl  28743  disjunsn  28789  esum2d  29482  omssubadd  29689  eulerpartlemgh  29767  eulerpartlemgs2  29769  bnj226  30056  bnj517  30209  bnj1118  30306  bnj1137  30317  cvmlift2lem12  30550  trpredlem1  30971  trpredss  30973  trpredmintr  30975  dftrpred3g  30977  frrlem5d  31031  frrlem7  31034  nofulllem5  31105  ntruni  31492  neibastop2lem  31525  filnetlem4  31546  mblfinlem2  32617  volsupnfl  32624  cnambfre  32628  sstotbnd2  32743  equivtotbnd  32747  totbndbnd  32758  prdstotbnd  32763  heiborlem1  32780  pclfinN  34204  lcfrlem4  35852  lcfrlem16  35865  lcfr  35892  iunrelexp0  37013  iunrelexpmin1  37019  iunrelexpmin2  37023  cotrcltrcl  37036  trclimalb2  37037  cotrclrcl  37053  iunconlem2  38193  ixpssmapc  38269  iunssd  38299  ioorrnopnlem  39200  omeiunle  39407  omeiunltfirp  39409  carageniuncl  39413  caratheodorylem1  39416  caratheodorylem2  39417  hoissrrn  39439  ovnlecvr  39448  ovnsubaddlem1  39460  ovnsubadd  39462  hoissrrn2  39468  ovnlecvr2  39500  hspmbl  39519  opnvonmbllem2  39523  vonvolmbllem  39550  vonvolmbl2  39553  vonvol2  39554  iunhoiioolem  39566  iunhoiioo  39567