Theorem uniexg 2871

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 2510	. . 3 |- (x = A -> U.x = U.A)
2	1	eleq1d 1540	. 2 |- (x = A -> (U.x e. V <-> U.A e. V))
3		visset 1813	. . 3 |- x e. V
4	3	uniex 2870	. 2 |- U.x e. V
5	2, 4	vtoclg 1847	1 |- (A e. B -> U.A e. V)

Syntax hints:   -> wi 3   = wceq 956   e. wcel 958  Vcvv 1811  U.cuni 2503

This theorem is referenced by:  euuni 2881  uniexb 2907  ssonunit 2994  dmexg 3358  rnexg 3359  iunexg 3862  tz7.44lem1 3927  carduni 4858  cardprc 4861  suplem2pr 5162  lbinfm 6048  eltopsp 7604  istps 7606  tgvalt 7616  eltgt 7618  eltg2t 7619  cldval 7666  ntrfval 7667  clsfval 7668  iscld 7669  ntrval 7676  clsval 7677  neifval 7714  neif 7715  neiss2 7716  neival 7717  isnei 7718  lpfval 7742  lpval 7743  islp2 7747  cnpfval 7757  iscn 7758  iscnp 7760  grpidval 8058  grpinvval 8067  grpinvf 8079  spwval2 8653  pjvalt 9239  fiv 10482  fivOLD 10483  homeofval 10516  idhme 10522  hmphre 10530  homcardus 10540  qusp 10555  fillsb 10560  cnfilca 10583  cnfilcaOLD 10584  sfvlim 10605  sfvlimOLD 10606  limfillem1OLD 10607

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-uni 2504

Copyright terms: Public domain