Theorem iunss 5048

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 4999	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 4010	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4057	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3968	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3092	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3282	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3181	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1820	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1538   ∈ wcel 2105  {cab 2708  ∀wral 3060  ∃wrex 3069   ⊆ wss 3948  ∪ ciun 4997

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-v 3475  df-in 3955  df-ss 3965  df-iun 4999

This theorem is referenced by:  iunss2  5052  iunssd  5053  djussxp  5845  fiun  7933  f1iun  7934  frrlem7  8283  wfrdmssOLD  8321  onfununi  8347  oawordeulem  8560  oaabslem  8652  oaabs2  8654  omabslem  8655  omabs  8656  marypha2lem1  9436  ttrclselem1  9726  trcl  9729  r1val1  9787  rankuni2b  9854  rankval4  9868  rankbnd  9869  rankbnd2  9870  rankc1  9871  cfslb2n  10269  cfsmolem  10271  hsmexlem2  10428  axdc3lem2  10452  ac6  10481  wuncval2  10748  inar1  10776  tskuni  10784  grur1a  10820  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  rtrclreclem4  15015  prmreclem4  16859  prmreclem5  16860  prdsval  17408  prdsbas  17410  imasaddfnlem  17481  imasvscafn  17490  imasvscaf  17492  isacs2  17604  mreacs  17609  acsfn  17610  dmcoass  18026  isacs5  18511  dprdspan  19945  dprd2dlem1  19959  dprd2d2  19962  dmdprdsplit2lem  19963  lbsextlem2  21006  lpival  21172  iunocv  21544  tgidm  22803  iunconn  23252  comppfsc  23356  txtube  23464  txcmplem2  23466  xkococnlem  23483  xkoinjcn  23511  alexsubALTlem3  23873  cnextf  23890  imasdsf1olem  24199  metnrmlem3  24697  ovolfiniun  25350  ovoliunlem2  25352  ovoliun  25354  ovoliunnul  25356  volfiniun  25396  voliunlem1  25399  volsup  25405  uniioombllem3a  25433  uniioombllem3  25434  uniioombllem4  25435  ismbf3d  25503  limciun  25743  taylfval  26210  taylf  26212  elpwiuncl  32198  disjunsn  32258  gsumpart  32643  esum2d  33555  omssubadd  33763  eulerpartlemgh  33841  eulerpartlemgs2  33843  bnj226  34209  bnj517  34360  bnj1118  34459  bnj1137  34470  cvmlift2lem12  34769  ntruni  35676  neibastop2lem  35709  filnetlem4  35730  mblfinlem2  36990  volsupnfl  36997  cnambfre  37000  sstotbnd2  37106  equivtotbnd  37110  totbndbnd  37121  prdstotbnd  37126  heiborlem1  37143  pclfinN  39235  lcfrlem4  40880  lcfrlem16  40893  lcfr  40920  oaabsb  42507  naddgeoa  42608  naddwordnexlem4  42615  iunrelexp0  42916  iunrelexpmin1  42922  iunrelexpmin2  42926  cotrcltrcl  42939  trclimalb2  42940  cotrclrcl  42956  iunconnlem2  44159  ixpssmapc  44223  ioorrnopnlem  45479  omeiunle  45692  omeiunltfirp  45694  carageniuncl  45698  caratheodorylem1  45701  caratheodorylem2  45702  hoissrrn  45724  ovnlecvr  45733  ovnsubaddlem1  45745  ovnsubadd  45747  hoissrrn2  45753  ovnlecvr2  45785  hspmbl  45804  opnvonmbllem2  45808  vonvolmbllem  45835  vonvolmbl2  45838  vonvol2  45839  iunhoiioolem  45850  iunhoiioo  45851