MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wununi Unicode version

Theorem wununi 9105
Description: A weak universe is closed under union. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wununi.1
wununi.2
Assertion
Ref Expression
wununi

Proof of Theorem wununi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wununi.2 . 2
2 wununi.1 . . 3
3 iswun 9103 . . . . 5
43ibi 241 . . . 4
54simp3d 1010 . . 3
6 simp1 996 . . . 4
76ralimi 2850 . . 3
82, 5, 73syl 20 . 2
9 unieq 4257 . . . 4
109eleq1d 2526 . . 3
1110rspcv 3206 . 2
121, 8, 11sylc 60 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807   c0 3784  ~Pcpw 4012  {cpr 4031  U.cuni 4249  Trwtr 4545   cwun 9099
This theorem is referenced by:  wunun  9109  wunint  9114  wundm  9127  wunrn  9128  wunfv  9131  intwun  9134  wuncval2  9146  wunstr  14651  wunfunc  15268  wunnat  15325  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250  df-tr 4546  df-wun 9101
  Copyright terms: Public domain W3C validator