Theorem iunss 4932

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 4883	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3943	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3988	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3901	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3133	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3198	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3238	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1821	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 301	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 300	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4883

This theorem is referenced by:  iunss2  4936  iunssd  4937  djussxp  5680  fiun  7626  f1iun  7627  wfrdmss  7944  onfununi  7961  oawordeulem  8163  oaabslem  8253  oaabs2  8255  omabslem  8256  omabs  8257  marypha2lem1  8883  trcl  9154  r1val1  9199  rankuni2b  9266  rankval4  9280  rankbnd  9281  rankbnd2  9282  rankc1  9283  cfslb2n  9679  cfsmolem  9681  hsmexlem2  9838  axdc3lem2  9862  ac6  9891  wuncval2  10158  inar1  10186  tskuni  10194  grur1a  10230  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  rtrclreclem4  14412  prmreclem4  16245  prmreclem5  16246  prdsval  16720  prdsbas  16722  imasaddfnlem  16793  imasvscafn  16802  imasvscaf  16804  isacs2  16916  mreacs  16921  acsfn  16922  dmcoass  17318  isacs5  17774  dprdspan  19142  dprd2dlem1  19156  dprd2d2  19159  dmdprdsplit2lem  19160  lbsextlem2  19924  lpival  20011  iunocv  20370  tgidm  21585  iunconn  22033  comppfsc  22137  txtube  22245  txcmplem2  22247  xkococnlem  22264  xkoinjcn  22292  alexsubALTlem3  22654  cnextf  22671  imasdsf1olem  22980  metnrmlem3  23466  ovolfiniun  24105  ovoliunlem2  24107  ovoliun  24109  ovoliunnul  24111  volfiniun  24151  voliunlem1  24154  volsup  24160  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  ismbf3d  24258  limciun  24497  taylfval  24954  taylf  24956  elpwiuncl  30300  disjunsn  30357  gsumpart  30740  esum2d  31462  omssubadd  31668  eulerpartlemgh  31746  eulerpartlemgs2  31748  bnj226  32114  bnj517  32267  bnj1118  32366  bnj1137  32377  cvmlift2lem12  32674  trpredlem1  33179  trpredss  33181  trpredmintr  33183  dftrpred3g  33185  frrlem7  33242  ntruni  33788  neibastop2lem  33821  filnetlem4  33842  mblfinlem2  35095  volsupnfl  35102  cnambfre  35105  sstotbnd2  35212  equivtotbnd  35216  totbndbnd  35227  prdstotbnd  35232  heiborlem1  35249  pclfinN  37196  lcfrlem4  38841  lcfrlem16  38854  lcfr  38881  iunrelexp0  40403  iunrelexpmin1  40409  iunrelexpmin2  40413  cotrcltrcl  40426  trclimalb2  40427  cotrclrcl  40443  iunconnlem2  41641  ixpssmapc  41708  ioorrnopnlem  42946  omeiunle  43156  omeiunltfirp  43158  carageniuncl  43162  caratheodorylem1  43165  caratheodorylem2  43166  hoissrrn  43188  ovnlecvr  43197  ovnsubaddlem1  43209  ovnsubadd  43211  hoissrrn2  43217  ovnlecvr2  43249  hspmbl  43268  opnvonmbllem2  43272  vonvolmbllem  43299  vonvolmbl2  43302  vonvol2  43303  iunhoiioolem  43314  iunhoiioo  43315