Theorem iunss 4969

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 4921	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3995	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 4040	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3955	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3165	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3235	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3279	. . . 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 2799  ∀wral 3138  ∃wrex 3139   ⊆ wss 3936  ∪ ciun 4919

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-in 3943  df-ss 3952  df-iun 4921

This theorem is referenced by:  iunss2  4973  iunssd  4974  djussxp  5716  fiun  7644  f1iun  7645  wfrdmss  7961  onfununi  7978  oawordeulem  8180  oaabslem  8270  oaabs2  8272  omabslem  8273  omabs  8274  marypha2lem1  8899  trcl  9170  r1val1  9215  rankuni2b  9282  rankval4  9296  rankbnd  9297  rankbnd2  9298  rankc1  9299  cfslb2n  9690  cfsmolem  9692  hsmexlem2  9849  axdc3lem2  9873  ac6  9902  wuncval2  10169  inar1  10197  tskuni  10205  grur1a  10241  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  wrdexgOLD  13873  rtrclreclem4  14420  prmreclem4  16255  prmreclem5  16256  prdsval  16728  prdsbas  16730  imasaddfnlem  16801  imasvscafn  16810  imasvscaf  16812  isacs2  16924  mreacs  16929  acsfn  16930  dmcoass  17326  isacs5  17782  dprdspan  19149  dprd2dlem1  19163  dprd2d2  19166  dmdprdsplit2lem  19167  lbsextlem2  19931  lpival  20018  iunocv  20825  tgidm  21588  iunconn  22036  comppfsc  22140  txtube  22248  txcmplem2  22250  xkococnlem  22267  xkoinjcn  22295  alexsubALTlem3  22657  cnextf  22674  imasdsf1olem  22983  metnrmlem3  23469  ovolfiniun  24102  ovoliunlem2  24104  ovoliun  24106  ovoliunnul  24108  volfiniun  24148  voliunlem1  24151  volsup  24157  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  ismbf3d  24255  limciun  24492  taylfval  24947  taylf  24949  elpwiuncl  30288  disjunsn  30344  esum2d  31352  omssubadd  31558  eulerpartlemgh  31636  eulerpartlemgs2  31638  bnj226  32004  bnj517  32157  bnj1118  32256  bnj1137  32267  cvmlift2lem12  32561  trpredlem1  33066  trpredss  33068  trpredmintr  33070  dftrpred3g  33072  frrlem7  33129  ntruni  33675  neibastop2lem  33708  filnetlem4  33729  mblfinlem2  34945  volsupnfl  34952  cnambfre  34955  sstotbnd2  35067  equivtotbnd  35071  totbndbnd  35082  prdstotbnd  35087  heiborlem1  35104  pclfinN  37051  lcfrlem4  38696  lcfrlem16  38709  lcfr  38736  iunrelexp0  40067  iunrelexpmin1  40073  iunrelexpmin2  40077  cotrcltrcl  40090  trclimalb2  40091  cotrclrcl  40107  iunconnlem2  41289  ixpssmapc  41356  ioorrnopnlem  42609  omeiunle  42819  omeiunltfirp  42821  carageniuncl  42825  caratheodorylem1  42828  caratheodorylem2  42829  hoissrrn  42851  ovnlecvr  42860  ovnsubaddlem1  42872  ovnsubadd  42874  hoissrrn2  42880  ovnlecvr2  42912  hspmbl  42931  opnvonmbllem2  42935  vonvolmbllem  42962  vonvolmbl2  42965  vonvol2  42966  iunhoiioolem  42977  iunhoiioo  42978