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

Theorem ifex 4133
Description: Conditional operator existence. (Contributed by NM, 2-Sep-2004.)
Hypotheses
Ref Expression
dedex.1 𝐴 ∈ V
dedex.2 𝐵 ∈ V
Assertion
Ref Expression
ifex if(𝜑, 𝐴, 𝐵) ∈ V

Proof of Theorem ifex
StepHypRef Expression
1 dedex.1 . 2 𝐴 ∈ V
2 dedex.2 . 2 𝐵 ∈ V
31, 2keepel 4132 1 if(𝜑, 𝐴, 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  Vcvv 3189  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-if 4064
This theorem is referenced by:  ifexg  4134  opex  4898  fnoe  7542  oev  7546  unxpdomlem1  8115  unxpdomlem2  8116  unxpdomlem3  8117  cantnflem1d  8536  cantnflem1  8537  iunfictbso  8888  fin23lem12  9104  axcc2lem  9209  ttukeylem3  9284  pwfseqlem2  9432  pwfseqlem3  9433  xnegex  11989  xaddval  12004  xmulval  12006  seqf1olem1  12787  expval  12809  bcval  13038  ccatlen  13306  ccatvalfn  13311  ccatalpha  13321  swrdval  13362  swrd00  13363  swrd0  13379  cshfn  13480  cshnz  13482  ofccat  13649  sgnval  13769  fsumser  14401  isumless  14509  rpnnen2lem1  14875  ruclem1  14892  sadcp1  15108  smupp1  15133  gcdval  15149  eucalgval2  15225  lcmval  15236  pcval  15480  pcmpt  15527  prmreclem2  15552  prmreclem5  15555  ramub1lem2  15662  ramcl  15664  acsfn  16248  gsumvalx  17198  mulgfval  17470  mulgval  17471  mulgfn  17472  odval  17881  odf  17884  gexval  17921  frgpup3lem  18118  dprdfeq0  18349  dmdprdsplitlem  18364  abvtrivd  18768  psrlidm  19331  psrridm  19332  mvrval2  19350  mplmonmul  19392  mplmon2  19421  coe1tmmul2fv  19576  coe1pwmulfv  19578  xrsdsval  19718  uvcvval  20053  mat1comp  20174  mat1ov  20182  matsc  20184  mat1dimid  20208  dmatmulcl  20234  scmatscmiddistr  20242  scmatscm  20247  mdetunilem9  20354  minmar1eval  20383  symgmatr01  20388  m2cpm  20474  m2cpminvid2lem  20487  decpmatid  20503  monmatcollpw  20512  mp2pm2mplem4  20542  chmatval  20562  chfacffsupp  20589  ptcmplem2  21776  ptcmplem3  21777  iccpnfhmeo  22663  xrhmeo  22664  phtpycc  22709  pcovalg  22731  pcohtpylem  22738  ovolunlem1a  23183  ovolunlem1  23184  ovolicc1  23203  ioorval  23261  mbfmax  23335  i1f1lem  23375  itg11  23377  itg1addlem3  23384  i1fres  23391  itg1climres  23400  mbfi1fseqlem4  23404  mbfi1fseqlem6  23406  mbfi1flimlem  23408  mbfi1flim  23409  itg2uba  23429  itg2splitlem  23434  itg2monolem1  23436  itg2gt0  23446  itg2cnlem1  23447  i1fibl  23493  itgeqa  23499  itgcn  23528  ditgex  23535  dvexp3  23658  ply1nzb  23799  ig1pval  23849  elply2  23869  dvply1  23956  aareccl  23998  dvtaylp  24041  pserdvlem2  24099  abelthlem9  24111  logtayl  24319  cxpval  24323  leibpilem2  24581  leibpi  24582  lgamgulmlem4  24671  lgamgulmlem5  24672  igamval  24686  vmaval  24752  vmaf  24758  muval  24771  prmorcht  24817  pclogsum  24853  dchrinvcl  24891  dchrptlem2  24903  bposlem5  24926  lgsval  24939  lgsfval  24940  lgsdir  24970  lgsdilem2  24971  lgsdi  24972  lgsne0  24973  gausslemma2dlem1  25004  pntrlog2bndlem4  25182  pntrlog2bndlem5  25183  padicval  25219  padicabv  25232  ostth1  25235  axlowdimlem15  25749  axlowdim  25754  vtxval  25791  iedgval  25792  vtxvalOLD  25793  iedgvalOLD  25794  crctcshwlkn0lem2  26585  crctcshwlkn0lem3  26586  clwlkclwwlklem2a2  26774  psgnfzto1stlem  29653  xrge0iifcv  29780  xrge0iifhom  29783  ddeval1  30096  ddeval0  30097  mrsubcv  31142  mrsubrn  31145  dfrdg2  31429  finxpreclem2  32886  finxpreclem5  32891  poimirlem2  33070  poimirlem24  33092  mblfinlem2  33106  itg2addnclem  33120  itg2addnclem2  33121  itg2addnclem3  33122  itg2addnc  33123  ftc1anclem5  33148  ftc1anclem7  33150  ftc1anclem8  33151  ftc1anc  33152  fdc  33200  renegclALT  33756  cdleme50f  35337  cdlemk40  35712  cdlemk56  35766  dihval  36028  dihf11lem  36062  mapdhval  36520  hdmap1vallem  36594  flcidc  37252  clsk1indlem2  37849  clsk1indlem3  37850  clsk1indlem4  37851  fourierdlem29  39681  fourierdlem56  39707  fourierswlem  39775  fouriersw  39776  nnfoctbdjlem  40000  isomenndlem  40072  hoidmvval  40119  hspmbl  40171  linc0scn0  41521  linc1  41523  lincext2  41553  blenval  41678
  Copyright terms: Public domain W3C validator