MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifexg Structured 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 3898 . . 3  |-  ( x  =  A  ->  if ( ph ,  x ,  y )  =  if ( ph ,  A ,  y ) )
21eleq1d 2521 . 2  |-  ( x  =  A  ->  ( if ( ph ,  x ,  y )  e. 
_V 
<->  if ( ph ,  A ,  y )  e.  _V ) )
3 ifeq2 3899 . . 3  |-  ( y  =  B  ->  if ( ph ,  A , 
y )  =  if ( ph ,  A ,  B ) )
43eleq1d 2521 . 2  |-  ( y  =  B  ->  ( if ( ph ,  A ,  y )  e. 
_V 
<->  if ( ph ,  A ,  B )  e.  _V ) )
5 vex 3075 . . 3  |-  x  e. 
_V
6 vex 3075 . . 3  |-  y  e. 
_V
75, 6ifex 3961 . 2  |-  if (
ph ,  x ,  y )  e.  _V
82, 4, 7vtocl2g 3134 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  if ( ph ,  A ,  B )  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370    e. wcel 1758   _Vcvv 3072   ifcif 3894
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 1954  ax-ext 2431
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-rab 2805  df-v 3074  df-un 3436  df-if 3895
This theorem is referenced by:  fsuppmptif  7755  cantnfp1lem1  7992  cantnfp1lem3  7994  cantnfp1lem1OLD  8018  cantnfp1lem3OLD  8020  symgextfv  16037  pmtrfv  16072  evlslem3  17719  marrepeval  18496  gsummatr01lem3  18590  stdbdmetval  20216  stdbdxmet  20217  ellimc2  21480  cdleme31fv  34353
  Copyright terms: Public domain W3C validator