Theorem uniexg 2862

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 2500	. . 3 |- (x = A -> U.x = U.A)
2	1	eleq1d 1532	. 2 |- (x = A -> (U.x e. V <-> U.A e. V))
3		visset 1804	. . 3 |- x e. V
4	3	uniex 2861	. 2 |- U.x e. V
5	2, 4	vtoclg 1838	1 |- (A e. B -> U.A e. V)

Syntax hints:   -> wi 3   = wceq 953   e. wcel 955  Vcvv 1802  U.cuni 2493

This theorem is referenced by:  euuni 2871  uniexb 2897  ssonunit 2984  dmexg 3344  rnexg 3345  iunexg 3847  tz7.44lem1 3912  pwuninelg 4467  carduni 4830  cardprc 4833  suplem2pr 5134  lbinfm 5995  eltopsp 7546  istps 7548  tgvalt 7558  eltgt 7560  eltg2t 7561  cldval 7608  ntrfval 7609  clsfval 7610  iscld 7611  ntrval 7618  clsval 7619  neifval 7655  neif 7656  neiss2 7657  neival 7658  isnei 7659  lpfval 7683  lpval 7684  islp2 7688  cnpfval 7697  iscn 7698  iscnp 7700  grpidval 7992  grpinvval 8001  grpinvf 8014  spwval2 8577  spwnex3 8579  pjvalt 9154  fiv 10374  homeofval 10403  idhme 10409  hmphre 10417  qusp 10430  fillsb 10435  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-uni 2494

Copyright terms: Public domain