Theorem iunss 5004

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2177, ax-12 2214. (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 3923	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4955	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 351	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1841	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3923	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3290	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3191	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1841	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
10	6, 7, 9	3bitrri 300	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
11	1, 4, 10	3bitri 299	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1560   ∈ wcel 2144  ∀wral 3078  ∃wrex 3088   ⊆ wss 3906  ∪ ciun 4951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-11 2193  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ral 3079  df-rex 3089  df-v 3458  df-ss 3923  df-iun 4953

This theorem is referenced by:  iunss2  5009  iunssd  5010  reliun  5791  djussxp  5819  fiun  7926  f1iun  7927  frrlem7  8275  onfununi  8314  oawordeulem  8525  oaabslem  8619  oaabs2  8621  omabslem  8622  omabs  8623  marypha2lem1  9383  ttrclselem1  9682  trcl  9685  r1val1  9746  rankuni2b  9813  rankval4  9827  rankbnd  9828  rankbnd2  9829  rankc1  9830  cfslb2n  10227  cfsmolem  10229  hsmexlem2  10386  axdc3lem2  10410  ac6  10439  wuncval2  10707  inar1  10735  tskuni  10743  grur1a  10779  fsuppmapnn0fiublem  14005  fsuppmapnn0fiub  14006  rtrclreclem4  15076  prmreclem4  16957  prmreclem5  16958  prdsval  17486  prdsbas  17488  imasaddfnlem  17560  imasvscafn  17569  imasvscaf  17571  isacs2  17687  mreacs  17692  acsfn  17693  dmcoass  18101  isacs5  18582  dprdspan  20071  dprd2dlem1  20085  dprd2d2  20088  dmdprdsplit2lem  20089  lbsextlem2  21231  lpival  21396  iunocv  21735  tgidm  23042  iunconn  23490  comppfsc  23594  txtube  23702  txcmplem2  23704  xkococnlem  23721  xkoinjcn  23749  alexsubALTlem3  24111  cnextf  24128  imasdsf1olem  24435  metnrmlem3  24924  ovolfiniun  25565  ovoliunlem2  25567  ovoliun  25569  ovoliunnul  25571  volfiniun  25611  voliunlem1  25614  volsup  25620  uniioombllem3a  25648  uniioombllem3  25649  uniioombllem4  25650  ismbf3d  25718  limciun  25958  taylfval  26424  taylf  26426  bdayle  28011  elpwiuncl  32728  disjunsn  32796  gsumpart  33245  esum2d  34392  omssubadd  34599  eulerpartlemgh  34677  eulerpartlemgs2  34679  bnj226  35032  bnj517  35182  bnj1118  35281  bnj1137  35292  rankval4b  35400  tz9.1regs  35434  cvmlift2lem12  35669  ntruni  36692  neibastop2lem  36725  filnetlem4  36746  ttciunun  36876  mblfinlem2  38162  volsupnfl  38169  cnambfre  38172  sstotbnd2  38278  equivtotbnd  38282  totbndbnd  38293  prdstotbnd  38298  heiborlem1  38315  pclfinN  40529  lcfrlem4  42174  lcfrlem16  42187  lcfr  42214  oaabsb  43876  naddgeoa  43976  naddwordnexlem4  43983  iunrelexp0  44283  iunrelexpmin1  44289  iunrelexpmin2  44293  cotrcltrcl  44306  trclimalb2  44307  cotrclrcl  44323  iunconnlem2  45515  ixpssmapc  45658  ioorrnopnlem  46883  omeiunle  47096  omeiunltfirp  47098  carageniuncl  47102  caratheodorylem1  47105  caratheodorylem2  47106  hoissrrn  47128  ovnlecvr  47137  ovnsubaddlem1  47149  ovnsubadd  47151  hoissrrn2  47157  ovnlecvr2  47189  hspmbl  47208  opnvonmbllem2  47212  vonvolmbllem  47239  vonvolmbl2  47242  vonvol2  47243  iunhoiioolem  47254  iunhoiioo  47255  iuneq0  49445  iuneqconst2  49449  imassc  49779