Theorem ifexg 4011

Description: Conditional operator existence. (Contributed by NM, 21-Mar-2011.)

Assertion

Ref	Expression
ifexg

Proof of Theorem ifexg

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ifeq1 3945	. . 3
2	1	eleq1d 2526	. 2
3		ifeq2 3946	. . 3
4	3	eleq1d 2526	. 2
5		vex 3112	. . 3
6		vex 3112	. . 3
7	5, 6	ifex 4010	. 2
8	2, 4, 7	vtocl2g 3171	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  cvv 3109  ifcif 3941

This theorem is referenced by:  fsuppmptif  7879  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  symgextfv  16443  pmtrfv  16477  evlslem3  18183  marrepeval  19065  gsummatr01lem3  19159  stdbdmetval  21017  stdbdxmet  21018  ellimc2  22281  cdleme31fv  36116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-un 3480  df-if 3942