Theorem iunss 5006

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2179, ax-12 2215. (Revised by SN, 2-Feb-2026.)

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-ss 3901	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4958	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1851	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3901	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3112	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3292	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3193	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1851	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 301	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 300	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   ∈ wcel 2146  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-11 2196  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4956

This theorem is used by:  iunss2  5011  iunssd  5012  reliun  5799  djussxp  5828  fiun  7965  f1iun  7966  frrlem7  8324  onfununi  8363  oawordeulem  8576  oaabslem  8670  oaabs2  8672  omabslem  8673  omabs  8674  marypha2lem1  9440  ttrclselem1  9739  trcl  9742  r1val1  9806  rankuni2b  9880  rankval4b  9893  rankval4  9897  rankbnd  9898  rankbnd2  9899  rankc1  9900  cfslb2n  10359  cfsmolem  10361  hsmexlem2  10518  axdc3lem2  10542  ac6  10571  wuncval2  10845  inar1  10873  tskuni  10881  grur1a  10917  fsuppmapnn0fiublem  14146  fsuppmapnn0fiub  14147  rtrclreclem4  15229  prmreclem4  17112  prmreclem5  17113  prdsval  17641  prdsbas  17643  imasaddfnlem  17715  imasvscafn  17724  imasvscaf  17726  isacs2  17842  mreacs  17847  acsfn  17848  dmcoass  18256  isacs5  18737  dprdspan  20258  dprd2dlem1  20272  dprd2d2  20275  dmdprdsplit2lem  20276  lbsextlem2  21452  lpival  21663  iunocv  22002  tgidm  23313  iunconn  23761  comppfsc  23866  txtube  23974  txcmplem2  23976  xkococnlem  23993  xkoinjcn  24021  alexsubALTlem3  24383  cnextf  24400  imasdsf1olem  24707  metnrmlem3  25196  ovolfiniun  25837  ovoliunlem2  25839  ovoliun  25841  ovoliunnul  25843  volfiniun  25883  voliunlem1  25886  volsup  25892  uniioombllem3a  25920  uniioombllem3  25921  uniioombllem4  25922  ismbf3d  25990  limciun  26229  taylfval  26701  taylf  26703  bdayle  28317  elpwiuncl  33180  disjunsn  33245  gsumpart  33680  esum2d  34781  omssubadd  34988  eulerpartlemgh  35066  eulerpartlemgs2  35068  bnj226  35421  bnj517  35571  bnj1118  35670  bnj1137  35681  tz9.1regs  35876  cvmlift2lem12  36203  ntruni  37248  neibastop2lem  37281  filnetlem4  37302  ttciunun  37432  mblfinlem2  38722  volsupnfl  38729  cnambfre  38732  sstotbnd2  38854  equivtotbnd  38858  totbndbnd  38869  prdstotbnd  38874  heiborlem1  38891  pclfinN  41103  lcfrlem4  42748  lcfrlem16  42761  lcfr  42788  oaabsb  44442  naddgeoa  44542  naddwordnexlem4  44549  iunrelexp0  44848  iunrelexpmin1  44854  iunrelexpmin2  44858  cotrcltrcl  44871  trclimalb2  44872  cotrclrcl  44888  iunconnlem2  46062  ixpssmapc  46235  ioorrnopnlem  47459  omeiunle  47672  omeiunltfirp  47674  carageniuncl  47678  caratheodorylem1  47681  caratheodorylem2  47682  hoissrrn  47704  ovnlecvr  47713  ovnsubaddlem1  47725  ovnsubadd  47727  hoissrrn2  47733  ovnlecvr2  47765  hspmbl  47784  opnvonmbllem2  47788  vonvolmbllem  47815  vonvolmbl2  47818  vonvol2  47819  iunhoiioolem  47830  iunhoiioo  47831  iuneq0  50075  iuneqconst2  50079  imassc  50414