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

Theorem eluniab 4251
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 4243 . 2  |-  ( A  e.  U. { x  |  ph }  <->  E. y
( A  e.  y  /\  y  e.  {
x  |  ph }
) )
2 nfv 1678 . . . 4  |-  F/ x  A  e.  y
3 nfsab1 2451 . . . 4  |-  F/ x  y  e.  { x  |  ph }
42, 3nfan 1870 . . 3  |-  F/ x
( A  e.  y  /\  y  e.  {
x  |  ph }
)
5 nfv 1678 . . 3  |-  F/ y ( A  e.  x  /\  ph )
6 eleq2 2535 . . . 4  |-  ( y  =  x  ->  ( A  e.  y  <->  A  e.  x ) )
7 eleq1 2534 . . . . 5  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  x  e.  { x  |  ph }
) )
8 abid 2449 . . . . 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 1990 . 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 1591    e. wcel 1762   {cab 2447   U.cuni 4240
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-uni 4241
This theorem is referenced by:  elunirab  4252  dfiun2g  4352  inuni  4604  elfv  5857  snnex  6579  unielxp  6812  tfrlem9  7046  dfac5lem2  8496  fin23lem30  8713  metrest  20757  aannenlem2  22454  fpwrelmapffslem  27215  wfrlem12  28919  frrlem11  28964  dfiota3  29138
  Copyright terms: Public domain W3C validator