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

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.
StepHypRef Expression
1 ifeq1 3945 . . 3
21eleq1d 2526 . 2
3 ifeq2 3946 . . 3
43eleq1d 2526 . 2
5 vex 3112 . . 3
6 vex 3112 . . 3
75, 6ifex 4010 . 2
82, 4, 7vtocl2g 3171 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator