Theorem iunss 4794

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 4755	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
2	1	sseq1i 3848	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶)
3		abss 3892	. 2 ⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} ⊆ 𝐶 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
4		dfss2 3809	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
5	4	ralbii 3162	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
6		ralcom4 3426	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦(𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
7		r19.23v 3205	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
8	7	albii 1863	. . 3 ⊢ (∀𝑦∀𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶))
9	5, 6, 8	3bitrri 290	. 2 ⊢ (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)
10	2, 3, 9	3bitri 289	1 ⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599   ∈ wcel 2107  {cab 2763  ∀wral 3090  ∃wrex 3091   ⊆ wss 3792  ∪ ciun 4753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400  df-in 3799  df-ss 3806  df-iun 4755

This theorem is referenced by:  iunss2  4798  djussxp  5513  fun11iun  7405  wfrdmss  7704  onfununi  7721  oawordeulem  7918  oaabslem  8007  oaabs2  8009  omabslem  8010  omabs  8011  marypha2lem1  8629  trcl  8901  r1val1  8946  rankuni2b  9013  rankval4  9027  rankbnd  9028  rankbnd2  9029  rankc1  9030  cfslb2n  9425  cfsmolem  9427  hsmexlem2  9584  axdc3lem2  9608  ac6  9637  wuncval2  9904  inar1  9932  tskuni  9940  grur1a  9976  fsuppmapnn0fiublem  13108  fsuppmapnn0fiub  13109  wrdexgOLD  13610  rtrclreclem4  14208  prmreclem4  16027  prmreclem5  16028  prdsval  16501  prdsbas  16503  imasaddfnlem  16574  imasaddflem  16576  imasvscafn  16583  imasvscaf  16585  isacs2  16699  mreacs  16704  acsfn  16705  dmcoass  17101  isacs5  17558  dprdspan  18813  dprd2dlem1  18827  dprd2d2  18830  dmdprdsplit2lem  18831  lbsextlem2  19556  lpival  19642  iunocv  20424  tgidm  21192  iunconn  21640  comppfsc  21744  txtube  21852  txcmplem2  21854  xkococnlem  21871  xkoinjcn  21899  alexsubALTlem3  22261  cnextf  22278  imasdsf1olem  22586  metnrmlem3  23072  ovolfiniun  23705  ovoliunlem2  23707  ovoliun  23709  ovoliunnul  23711  volfiniun  23751  voliunlem1  23754  volsup  23760  uniioombllem3a  23788  uniioombllem3  23789  uniioombllem4  23790  ismbf3d  23858  limciun  24095  taylfval  24550  taylf  24552  elpwiuncl  29921  disjunsn  29970  esum2d  30753  omssubadd  30960  eulerpartlemgh  31038  eulerpartlemgs2  31040  bnj226  31402  bnj517  31554  bnj1118  31651  bnj1137  31662  cvmlift2lem12  31895  trpredlem1  32315  trpredss  32317  trpredmintr  32319  dftrpred3g  32321  frrlem5d  32376  frrlem7  32379  ntruni  32910  neibastop2lem  32943  filnetlem4  32964  mblfinlem2  34075  volsupnfl  34082  cnambfre  34085  sstotbnd2  34199  equivtotbnd  34203  totbndbnd  34214  prdstotbnd  34219  heiborlem1  34236  pclfinN  36056  lcfrlem4  37701  lcfrlem16  37714  lcfr  37741  iunrelexp0  38955  iunrelexpmin1  38961  iunrelexpmin2  38965  cotrcltrcl  38978  trclimalb2  38979  cotrclrcl  38995  iunconnlem2  40108  ixpssmapc  40178  iunssd  40206  ioorrnopnlem  41452  omeiunle  41662  omeiunltfirp  41664  carageniuncl  41668  caratheodorylem1  41671  caratheodorylem2  41672  hoissrrn  41694  ovnlecvr  41703  ovnsubaddlem1  41715  ovnsubadd  41717  hoissrrn2  41723  ovnlecvr2  41755  hspmbl  41774  opnvonmbllem2  41778  vonvolmbllem  41805  vonvolmbl2  41808  vonvol2  41809  iunhoiioolem  41820  iunhoiioo  41821