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

Theorem eluniab 4200
Description: Membership in union of a class abstraction. (Contributed by NM, 11-Aug-1994.) (Revised by Mario Carneiro, 14-Nov-2016.)
Assertion
Ref Expression
eluniab  |-  ( A  e.  U. { x  |  ph }  <->  E. x
( A  e.  x  /\  ph ) )
Distinct variable group:    x, A
Allowed substitution hint:    ph( x)

Proof of Theorem eluniab
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eluni 4192 . 2  |-  ( A  e.  U. { x  |  ph }  <->  E. y
( A  e.  y  /\  y  e.  {
x  |  ph }
) )
2 nfv 1674 . . . 4  |-  F/ x  A  e.  y
3 nfsab1 2440 . . . 4  |-  F/ x  y  e.  { x  |  ph }
42, 3nfan 1863 . . 3  |-  F/ x
( A  e.  y  /\  y  e.  {
x  |  ph }
)
5 nfv 1674 . . 3  |-  F/ y ( A  e.  x  /\  ph )
6 eleq2 2524 . . . 4  |-  ( y  =  x  ->  ( A  e.  y  <->  A  e.  x ) )
7 eleq1 2523 . . . . 5  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  x  e.  { x  |  ph }
) )
8 abid 2438 . . . . 5  |-  ( x  e.  { x  | 
ph }  <->  ph )
97, 8syl6bb 261 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
106, 9anbi12d 710 . . 3  |-  ( y  =  x  ->  (
( A  e.  y  /\  y  e.  {
x  |  ph }
)  <->  ( A  e.  x  /\  ph )
) )
114, 5, 10cbvex 1979 . 2  |-  ( E. y ( A  e.  y  /\  y  e. 
{ x  |  ph } )  <->  E. x
( A  e.  x  /\  ph ) )
121, 11bitri 249 1  |-  ( A  e.  U. { x  |  ph }  <->  E. x
( A  e.  x  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1587    e. wcel 1758   {cab 2436   U.cuni 4189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-uni 4190
This theorem is referenced by:  elunirab  4201  dfiun2g  4300  inuni  4552  elfv  5787  snnex  6482  unielxp  6712  tfrlem9  6944  dfac5lem2  8395  fin23lem30  8612  metrest  20215  aannenlem2  21911  fpwrelmapffslem  26166  wfrlem12  27869  frrlem11  27914  dfiota3  28088
  Copyright terms: Public domain W3C validator