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

Theorem eluniab 4204
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 4196 . 2  |-  ( A  e.  U. { x  |  ph }  <->  E. y
( A  e.  y  /\  y  e.  {
x  |  ph }
) )
2 nfv 1730 . . . 4  |-  F/ x  A  e.  y
3 nfsab1 2393 . . . 4  |-  F/ x  y  e.  { x  |  ph }
42, 3nfan 1958 . . 3  |-  F/ x
( A  e.  y  /\  y  e.  {
x  |  ph }
)
5 nfv 1730 . . 3  |-  F/ y ( A  e.  x  /\  ph )
6 eleq2 2477 . . . 4  |-  ( y  =  x  ->  ( A  e.  y  <->  A  e.  x ) )
7 eleq1 2476 . . . . 5  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  x  e.  { x  |  ph }
) )
8 abid 2391 . . . . 5  |-  ( x  e.  { x  | 
ph }  <->  ph )
97, 8syl6bb 263 . . . 4  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  ph ) )
106, 9anbi12d 711 . . 3  |-  ( y  =  x  ->  (
( A  e.  y  /\  y  e.  {
x  |  ph }
)  <->  ( A  e.  x  /\  ph )
) )
114, 5, 10cbvex 2051 . 2  |-  ( E. y ( A  e.  y  /\  y  e. 
{ x  |  ph } )  <->  E. x
( A  e.  x  /\  ph ) )
121, 11bitri 251 1  |-  ( A  e.  U. { x  |  ph }  <->  E. x
( A  e.  x  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 186    /\ wa 369   E.wex 1635    e. wcel 1844   {cab 2389   U.cuni 4193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-v 3063  df-uni 4194
This theorem is referenced by:  elunirab  4205  dfiun2g  4305  inuni  4558  elfv  5849  snnex  6590  unielxp  6822  wfrlem12  7034  tfrlem9  7090  dfac5lem2  8539  fin23lem30  8756  unisngl  20322  metrest  21321  aannenlem2  23019  fpwrelmapffslem  28015  frrlem11  30112  dfiota3  30274  mptsnunlem  31267
  Copyright terms: Public domain W3C validator