Theorem iunss 5045

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 4993	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 4012	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4063	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		df-ss 3968	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3093	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3286	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3183	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1819	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 298	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 297	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070   ⊆ wss 3951  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-ss 3968  df-iun 4993

This theorem is referenced by:  iunss2  5049  iunssd  5050  djussxp  5856  fiun  7967  f1iun  7968  frrlem7  8317  wfrdmssOLD  8355  onfununi  8381  oawordeulem  8592  oaabslem  8685  oaabs2  8687  omabslem  8688  omabs  8689  marypha2lem1  9475  ttrclselem1  9765  trcl  9768  r1val1  9826  rankuni2b  9893  rankval4  9907  rankbnd  9908  rankbnd2  9909  rankc1  9910  cfslb2n  10308  cfsmolem  10310  hsmexlem2  10467  axdc3lem2  10491  ac6  10520  wuncval2  10787  inar1  10815  tskuni  10823  grur1a  10859  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  rtrclreclem4  15100  prmreclem4  16957  prmreclem5  16958  prdsval  17500  prdsbas  17502  imasaddfnlem  17573  imasvscafn  17582  imasvscaf  17584  isacs2  17696  mreacs  17701  acsfn  17702  dmcoass  18111  isacs5  18593  dprdspan  20047  dprd2dlem1  20061  dprd2d2  20064  dmdprdsplit2lem  20065  lbsextlem2  21161  lpival  21334  iunocv  21699  tgidm  22987  iunconn  23436  comppfsc  23540  txtube  23648  txcmplem2  23650  xkococnlem  23667  xkoinjcn  23695  alexsubALTlem3  24057  cnextf  24074  imasdsf1olem  24383  metnrmlem3  24883  ovolfiniun  25536  ovoliunlem2  25538  ovoliun  25540  ovoliunnul  25542  volfiniun  25582  voliunlem1  25585  volsup  25591  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  ismbf3d  25689  limciun  25929  taylfval  26400  taylf  26402  elpwiuncl  32546  disjunsn  32607  gsumpart  33060  esum2d  34094  omssubadd  34302  eulerpartlemgh  34380  eulerpartlemgs2  34382  bnj226  34748  bnj517  34899  bnj1118  34998  bnj1137  35009  cvmlift2lem12  35319  ntruni  36328  neibastop2lem  36361  filnetlem4  36382  mblfinlem2  37665  volsupnfl  37672  cnambfre  37675  sstotbnd2  37781  equivtotbnd  37785  totbndbnd  37796  prdstotbnd  37801  heiborlem1  37818  pclfinN  39902  lcfrlem4  41547  lcfrlem16  41560  lcfr  41587  oaabsb  43307  naddgeoa  43407  naddwordnexlem4  43414  iunrelexp0  43715  iunrelexpmin1  43721  iunrelexpmin2  43725  cotrcltrcl  43738  trclimalb2  43739  cotrclrcl  43755  iunconnlem2  44955  ixpssmapc  45078  ioorrnopnlem  46319  omeiunle  46532  omeiunltfirp  46534  carageniuncl  46538  caratheodorylem1  46541  caratheodorylem2  46542  hoissrrn  46564  ovnlecvr  46573  ovnsubaddlem1  46585  ovnsubadd  46587  hoissrrn2  46593  ovnlecvr2  46625  hspmbl  46644  opnvonmbllem2  46648  vonvolmbllem  46675  vonvolmbl2  46678  vonvol2  46679  iunhoiioolem  46690  iunhoiioo  46691