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

Theorem ifex 4296
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 4295 1 if(𝜑, 𝐴, 𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2135  Vcvv 3336  ifcif 4226
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-clab 2743  df-cleq 2749  df-clel 2752  df-if 4227
This theorem is referenced by:  ifexg  4297  opex  5077  fnoe  7755  oev  7759  unxpdomlem1  8325  unxpdomlem2  8326  unxpdomlem3  8327  cantnflem1d  8754  cantnflem1  8755  iunfictbso  9123  fin23lem12  9341  axcc2lem  9446  ttukeylem3  9521  pwfseqlem2  9669  pwfseqlem3  9670  xnegex  12228  xaddval  12243  xmulval  12245  seqf1olem1  13030  expval  13052  bcval  13281  ccatlen  13543  ccatvalfn  13549  ccatalpha  13561  swrdval  13612  swrd00  13613  swrd0  13630  cshfn  13732  cshnz  13734  ofccat  13905  sgnval  14023  fsumser  14656  isumless  14772  rpnnen2lem1  15138  ruclem1  15155  sadcp1  15375  smupp1  15400  gcdval  15416  eucalgval2  15492  lcmval  15503  pcval  15747  pcmpt  15794  prmreclem2  15819  prmreclem5  15822  ramub1lem2  15929  ramcl  15931  acsfn  16517  gsumvalx  17467  mulgfval  17739  mulgval  17740  mulgfn  17741  odval  18149  odf  18152  gexval  18189  frgpup3lem  18386  dprdfeq0  18617  dmdprdsplitlem  18632  abvtrivd  19038  psrlidm  19601  psrridm  19602  mvrval2  19620  mplmonmul  19662  mplmon2  19691  coe1tmmul2fv  19846  coe1pwmulfv  19848  xrsdsval  19988  uvcvval  20323  mat1comp  20444  mat1ov  20452  matsc  20454  mat1dimid  20478  dmatmulcl  20504  scmatscmiddistr  20512  scmatscm  20517  mdetunilem9  20624  minmar1eval  20653  symgmatr01  20658  m2cpm  20744  m2cpminvid2lem  20757  decpmatid  20773  monmatcollpw  20782  mp2pm2mplem4  20812  chmatval  20832  chfacffsupp  20859  ptcmplem2  22054  ptcmplem3  22055  iccpnfhmeo  22941  xrhmeo  22942  phtpycc  22987  pcovalg  23008  pcohtpylem  23015  ovolunlem1a  23460  ovolunlem1  23461  ovolicc1  23480  ioorval  23538  mbfmax  23611  i1f1lem  23651  itg11  23653  itg1addlem3  23660  i1fres  23667  itg1climres  23676  mbfi1fseqlem4  23680  mbfi1fseqlem6  23682  mbfi1flimlem  23684  mbfi1flim  23685  itg2uba  23705  itg2splitlem  23710  itg2monolem1  23712  itg2gt0  23722  itg2cnlem1  23723  i1fibl  23769  itgeqa  23775  itgcn  23804  ditgex  23811  dvexp3  23936  ply1nzb  24077  ig1pval  24127  elply2  24147  dvply1  24234  aareccl  24276  dvtaylp  24319  pserdvlem2  24377  abelthlem9  24389  logtayl  24601  cxpval  24605  leibpilem2  24863  leibpi  24864  lgamgulmlem4  24953  lgamgulmlem5  24954  igamval  24968  vmaval  25034  vmaf  25040  muval  25053  prmorcht  25099  pclogsum  25135  dchrinvcl  25173  dchrptlem2  25185  bposlem5  25208  lgsval  25221  lgsfval  25222  lgsdir  25252  lgsdilem2  25253  lgsdi  25254  lgsne0  25255  gausslemma2dlem1  25286  pntrlog2bndlem4  25464  pntrlog2bndlem5  25465  padicval  25501  padicabv  25514  ostth1  25517  axlowdimlem15  26031  axlowdim  26036  vtxval  26073  iedgval  26074  vtxvalOLD  26075  iedgvalOLD  26076  crctcshwlkn0lem2  26910  crctcshwlkn0lem3  26911  clwlkclwwlklem2a2  27112  psgnfzto1stlem  30155  xrge0iifcv  30285  xrge0iifhom  30288  ddeval1  30602  ddeval0  30603  mrsubcv  31710  mrsubrn  31713  dfrdg2  32002  finxpreclem2  33534  finxpreclem5  33539  poimirlem2  33720  poimirlem24  33742  mblfinlem2  33756  itg2addnclem  33770  itg2addnclem2  33771  itg2addnclem3  33772  itg2addnc  33773  ftc1anclem5  33798  ftc1anclem7  33800  ftc1anclem8  33801  ftc1anc  33802  fdc  33850  renegclALT  34748  cdleme50f  36328  cdlemk40  36703  cdlemk56  36757  dihval  37019  dihf11lem  37053  mapdhval  37511  hdmap1vallem  37585  flcidc  38242  clsk1indlem2  38838  clsk1indlem3  38839  clsk1indlem4  38840  limsup10exlem  40503  fourierdlem29  40852  fourierdlem56  40878  fourierswlem  40946  fouriersw  40947  nnfoctbdjlem  41171  isomenndlem  41246  hoidmvval  41293  hspmbl  41345  linc0scn0  42718  linc1  42720  lincext2  42750  blenval  42871
  Copyright terms: Public domain W3C validator