Theorem uniexg 2877

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A e. B instead of A e. V to make the theorem more general and thus shorten some proofs; obviously V is one possibility for B.

Assertion

Ref	Expression
uniexg	|- (A e. B -> U.A e. V)

Proof of Theorem uniexg

Step	Hyp	Ref	Expression
1		unieq 2514	. . 3 |- (x = A -> U.x = U.A)
2	1	eleq1d 1543	. 2 |- (x = A -> (U.x e. V <-> U.A e. V))
3		visset 1816	. . 3 |- x e. V
4	3	uniex 2876	. 2 |- U.x e. V
5	2, 4	vtoclg 1850	1 |- (A e. B -> U.A e. V)

Syntax hints:   -> wi 3   = wceq 958   e. wcel 960  Vcvv 1814  U.cuni 2507

This theorem is referenced by:  euuni 2887  uniexb 2913  ssonunit 3000  dmexg 3364  rnexg 3365  iunexg 3868  tz7.44lem1 3933  carduni 4869  cardprc 4872  suplem2pr 5174  lbinfm 6050  eltopsp 7605  istps 7607  tgvalt 7615  eltgt 7617  eltg2t 7618  cldval 7663  ntrfval 7664  clsfval 7665  iscld 7666  ntrval 7673  clsval 7674  neifval 7711  neif 7712  neiss2 7713  neival 7714  isnei 7715  lpfval 7739  lpval 7740  islp2 7744  cnpfval 7754  iscn 7755  iscnp 7757  grpidval 8054  grpinvval 8063  grpinvf 8075  spwval2 8649  pjvalt 9234  fiv 10470  homeofval 10502  idhme 10508  hmphre 10516  homcardus 10526  qusp 10541  fillsb 10546  cnfilca 10562  sfvlim 10576  sfvlimOLD 10577  limfillem1OLD 10578

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-sep 2708  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-uni 2508

Copyright terms: Public domain