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

Theorem eluniab 4095
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 4087 . 2  |-  ( A  e.  U. { x  |  ph }  <->  E. y
( A  e.  y  /\  y  e.  {
x  |  ph }
) )
2 nfv 1673 . . . 4  |-  F/ x  A  e.  y
3 nfsab1 2427 . . . 4  |-  F/ x  y  e.  { x  |  ph }
42, 3nfan 1860 . . 3  |-  F/ x
( A  e.  y  /\  y  e.  {
x  |  ph }
)
5 nfv 1673 . . 3  |-  F/ y ( A  e.  x  /\  ph )
6 eleq2 2498 . . . 4  |-  ( y  =  x  ->  ( A  e.  y  <->  A  e.  x ) )
7 eleq1 2497 . . . . 5  |-  ( y  =  x  ->  (
y  e.  { x  |  ph }  <->  x  e.  { x  |  ph }
) )
8 abid 2425 . . . . 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 1970 . 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 1586    e. wcel 1756   {cab 2423   U.cuni 4084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-v 2968  df-uni 4085
This theorem is referenced by:  elunirab  4096  dfiun2g  4195  inuni  4447  elfv  5682  snnex  6377  unielxp  6607  tfrlem9  6836  dfac5lem2  8286  fin23lem30  8503  metrest  20068  aannenlem2  21764  fpwrelmapffslem  25977  wfrlem12  27682  frrlem11  27727  dfiota3  27901
  Copyright terms: Public domain W3C validator