Theorem iunss 4971

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 4923	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3997	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4042	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3957	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3167	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3237	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3281	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1820	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 300	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 299	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  {cab 2801  ∀wral 3140  ∃wrex 3141   ⊆ wss 3938  ∪ ciun 4921

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-in 3945  df-ss 3954  df-iun 4923

This theorem is referenced by:  iunss2  4975  iunssd  4976  djussxp  5718  fiun  7646  f1iun  7647  wfrdmss  7963  onfununi  7980  oawordeulem  8182  oaabslem  8272  oaabs2  8274  omabslem  8275  omabs  8276  marypha2lem1  8901  trcl  9172  r1val1  9217  rankuni2b  9284  rankval4  9298  rankbnd  9299  rankbnd2  9300  rankc1  9301  cfslb2n  9692  cfsmolem  9694  hsmexlem2  9851  axdc3lem2  9875  ac6  9904  wuncval2  10171  inar1  10199  tskuni  10207  grur1a  10243  fsuppmapnn0fiublem  13361  fsuppmapnn0fiub  13362  wrdexgOLD  13875  rtrclreclem4  14422  prmreclem4  16257  prmreclem5  16258  prdsval  16730  prdsbas  16732  imasaddfnlem  16803  imasvscafn  16812  imasvscaf  16814  isacs2  16926  mreacs  16931  acsfn  16932  dmcoass  17328  isacs5  17784  dprdspan  19151  dprd2dlem1  19165  dprd2d2  19168  dmdprdsplit2lem  19169  lbsextlem2  19933  lpival  20020  iunocv  20827  tgidm  21590  iunconn  22038  comppfsc  22142  txtube  22250  txcmplem2  22252  xkococnlem  22269  xkoinjcn  22297  alexsubALTlem3  22659  cnextf  22676  imasdsf1olem  22985  metnrmlem3  23471  ovolfiniun  24104  ovoliunlem2  24106  ovoliun  24108  ovoliunnul  24110  volfiniun  24150  voliunlem1  24153  volsup  24159  uniioombllem3a  24187  uniioombllem3  24188  uniioombllem4  24189  ismbf3d  24257  limciun  24494  taylfval  24949  taylf  24951  elpwiuncl  30290  disjunsn  30346  esum2d  31354  omssubadd  31560  eulerpartlemgh  31638  eulerpartlemgs2  31640  bnj226  32006  bnj517  32159  bnj1118  32258  bnj1137  32269  cvmlift2lem12  32563  trpredlem1  33068  trpredss  33070  trpredmintr  33072  dftrpred3g  33074  frrlem7  33131  ntruni  33677  neibastop2lem  33710  filnetlem4  33731  mblfinlem2  34932  volsupnfl  34939  cnambfre  34942  sstotbnd2  35054  equivtotbnd  35058  totbndbnd  35069  prdstotbnd  35074  heiborlem1  35091  pclfinN  37038  lcfrlem4  38683  lcfrlem16  38696  lcfr  38723  iunrelexp0  40054  iunrelexpmin1  40060  iunrelexpmin2  40064  cotrcltrcl  40077  trclimalb2  40078  cotrclrcl  40094  iunconnlem2  41276  ixpssmapc  41343  ioorrnopnlem  42596  omeiunle  42806  omeiunltfirp  42808  carageniuncl  42812  caratheodorylem1  42815  caratheodorylem2  42816  hoissrrn  42838  ovnlecvr  42847  ovnsubaddlem1  42859  ovnsubadd  42861  hoissrrn2  42867  ovnlecvr2  42899  hspmbl  42918  opnvonmbllem2  42922  vonvolmbllem  42949  vonvolmbl2  42952  vonvol2  42953  iunhoiioolem  42964  iunhoiioo  42965