Theorem ifexg 4157

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.

Step	Hyp	Ref	Expression
1		ifeq1 4090	. . 3 |- ( x = A -> if ( ph , x , y ) = if ( ph , A , y ) )
2	1	eleq1d 2686	. 2 |- ( x = A -> ( if ( ph , x , y ) e. _V <-> if ( ph , A , y ) e. _V ) )
3		ifeq2 4091	. . 3 |- ( y = B -> if ( ph , A , y ) = if ( ph , A , B ) )
4	3	eleq1d 2686	. 2 |- ( y = B -> ( if ( ph , A , y ) e. _V <-> if ( ph , A , B ) e. _V ) )
5		vex 3203	. . 3 |- x e. _V
6		vex 3203	. . 3 |- y e. _V
7	5, 6	ifex 4156	. 2 |- if ( ph , x , y ) e. _V
8	2, 4, 7	vtocl2g 3270	1 |- ( ( A e. V /\ B e. W ) -> if ( ph , A , B ) e. _V )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  fsuppmptif  8305  cantnfp1lem1  8575  cantnfp1lem3  8577  symgextfv  17838  pmtrfv  17872  evlslem3  19514  marrepeval  20369  gsummatr01lem3  20463  stdbdmetval  22319  stdbdxmet  22320  ellimc2  23641  psgnfzto1stlem  29850  cdleme31fv  35678  sge0val  40583  hsphoival  40793  hspmbllem2  40841