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

Theorem ifexg 3962
Description: Conditional operator existence. (Contributed by NM, 21-Mar-2011.)
Assertion
Ref Expression
ifexg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  if ( ph ,  A ,  B )  e.  _V )

Proof of Theorem ifexg
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ifeq1 3897 . . 3  |-  ( x  =  A  ->  if ( ph ,  x ,  y )  =  if ( ph ,  A ,  y ) )
21eleq1d 2524 . 2  |-  ( x  =  A  ->  ( if ( ph ,  x ,  y )  e. 
_V 
<->  if ( ph ,  A ,  y )  e.  _V ) )
3 ifeq2 3898 . . 3  |-  ( y  =  B  ->  if ( ph ,  A , 
y )  =  if ( ph ,  A ,  B ) )
43eleq1d 2524 . 2  |-  ( y  =  B  ->  ( if ( ph ,  A ,  y )  e. 
_V 
<->  if ( ph ,  A ,  B )  e.  _V ) )
5 vex 3060 . . 3  |-  x  e. 
_V
6 vex 3060 . . 3  |-  y  e. 
_V
75, 6ifex 3961 . 2  |-  if (
ph ,  x ,  y )  e.  _V
82, 4, 7vtocl2g 3123 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  if ( ph ,  A ,  B )  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   _Vcvv 3057   ifcif 3893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-un 3421  df-if 3894
This theorem is referenced by:  fsuppmptif  7939  cantnfp1lem1  8209  cantnfp1lem3  8211  symgextfv  17108  pmtrfv  17142  evlslem3  18786  marrepeval  19637  gsummatr01lem3  19731  stdbdmetval  21578  stdbdxmet  21579  ellimc2  22881  psgnfzto1stlem  28662  cdleme31fv  34002  sge0val  38246  hsphoival  38439  hspmbllem2  38487
  Copyright terms: Public domain W3C validator