Theorem iunss 5003

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Avoid ax-10 2178, ax-12 2213. (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 3916	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶))
2		eliun 4955	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)
3	2	imbi1i 352	. . 3 ⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4	3	albii 1852	. 2 ⊢ (∀𝑦(𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5		df-ss 3916	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6	5	ralbii 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		ralcom4 3288	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8		r19.23v 3189	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	8	albii 1852	. . 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 1568   ∈ wcel 2145  ∀wral 3076  ∃wrex 3086   ⊆ wss 3899  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3916  df-iun 4953

This theorem is used by:  iunss2  5008  iunssd  5009  reliun  5797  djussxp  5825  fiun  7941  f1iun  7942  frrlem7  8292  onfununi  8331  oawordeulem  8544  oaabslem  8638  oaabs2  8640  omabslem  8641  omabs  8642  marypha2lem1  9408  ttrclselem1  9707  trcl  9710  r1val1  9771  rankuni2b  9838  rankval4  9852  rankbnd  9853  rankbnd2  9854  rankc1  9855  cfslb2n  10273  cfsmolem  10275  hsmexlem2  10432  axdc3lem2  10456  ac6  10485  wuncval2  10759  inar1  10787  tskuni  10795  grur1a  10831  fsuppmapnn0fiublem  14057  fsuppmapnn0fiub  14058  rtrclreclem4  15137  prmreclem4  17014  prmreclem5  17015  prdsval  17543  prdsbas  17545  imasaddfnlem  17617  imasvscafn  17626  imasvscaf  17628  isacs2  17744  mreacs  17749  acsfn  17750  dmcoass  18158  isacs5  18639  dprdspan  20159  dprd2dlem1  20173  dprd2d2  20176  dmdprdsplit2lem  20177  lbsextlem2  21349  lpival  21558  iunocv  21897  tgidm  23208  iunconn  23656  comppfsc  23761  txtube  23869  txcmplem2  23871  xkococnlem  23888  xkoinjcn  23916  alexsubALTlem3  24278  cnextf  24295  imasdsf1olem  24602  metnrmlem3  25091  ovolfiniun  25732  ovoliunlem2  25734  ovoliun  25736  ovoliunnul  25738  volfiniun  25778  voliunlem1  25781  volsup  25787  uniioombllem3a  25815  uniioombllem3  25816  uniioombllem4  25817  ismbf3d  25885  limciun  26124  taylfval  26598  taylf  26600  bdayle  28184  elpwiuncl  33005  disjunsn  33070  gsumpart  33506  esum2d  34606  omssubadd  34814  eulerpartlemgh  34892  eulerpartlemgs2  34894  bnj226  35247  bnj517  35397  bnj1118  35496  bnj1137  35507  rankval4b  35610  tz9.1regs  35663  cvmlift2lem12  35896  ntruni  36949  neibastop2lem  36982  filnetlem4  37003  ttciunun  37133  mblfinlem2  38410  volsupnfl  38417  cnambfre  38420  sstotbnd2  38527  equivtotbnd  38531  totbndbnd  38542  prdstotbnd  38547  heiborlem1  38564  pclfinN  40776  lcfrlem4  42421  lcfrlem16  42434  lcfr  42461  oaabsb  44138  naddgeoa  44238  naddwordnexlem4  44245  iunrelexp0  44545  iunrelexpmin1  44551  iunrelexpmin2  44555  cotrcltrcl  44568  trclimalb2  44569  cotrclrcl  44585  iunconnlem2  45760  ixpssmapc  45910  ioorrnopnlem  47135  omeiunle  47348  omeiunltfirp  47350  carageniuncl  47354  caratheodorylem1  47357  caratheodorylem2  47358  hoissrrn  47380  ovnlecvr  47389  ovnsubaddlem1  47401  ovnsubadd  47403  hoissrrn2  47409  ovnlecvr2  47441  hspmbl  47460  opnvonmbllem2  47464  vonvolmbllem  47491  vonvolmbl2  47494  vonvol2  47495  iunhoiioolem  47506  iunhoiioo  47507  iuneq0  49750  iuneqconst2  49754  imassc  50082