Theorem ifex 4106

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

Step	Hyp	Ref	Expression
1		dedex.1	. 2 ⊢ 𝐴 ∈ V
2		dedex.2	. 2 ⊢ 𝐵 ∈ V
3	1, 2	keepel 4105	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  ifexg  4107  opex  4859  fnoe  7477  oev  7481  unxpdomlem1  8049  unxpdomlem2  8050  unxpdomlem3  8051  cantnflem1d  8468  cantnflem1  8469  iunfictbso  8820  fin23lem12  9036  axcc2lem  9141  ttukeylem3  9216  pwfseqlem2  9360  pwfseqlem3  9361  xnegex  11913  xaddval  11928  xmulval  11930  seqf1olem1  12702  expval  12724  bcval  12953  ccatlen  13213  ccatvalfn  13218  ccatalpha  13228  swrdval  13269  swrd00  13270  swrd0  13286  cshfn  13387  cshnz  13389  ofccat  13556  sgnval  13676  fsumser  14308  isumless  14416  rpnnen2lem1  14782  ruclem1  14799  sadcp1  15015  smupp1  15040  gcdval  15056  eucalgval2  15132  lcmval  15143  pcval  15387  pcmpt  15434  prmreclem2  15459  prmreclem5  15462  ramub1lem2  15569  ramcl  15571  acsfn  16143  gsumvalx  17093  mulgfval  17365  mulgval  17366  mulgfn  17367  odval  17776  odf  17779  gexval  17816  frgpup3lem  18013  dprdfeq0  18244  dmdprdsplitlem  18259  abvtrivd  18663  psrlidm  19224  psrridm  19225  mvrval2  19243  mplmonmul  19285  mplmon2  19314  coe1tmmul2fv  19469  coe1pwmulfv  19471  xrsdsval  19609  uvcvval  19944  mat1comp  20065  mat1ov  20073  matsc  20075  mat1dimid  20099  dmatmulcl  20125  scmatscmiddistr  20133  scmatscm  20138  mdetunilem9  20245  minmar1eval  20274  symgmatr01  20279  m2cpm  20365  m2cpminvid2lem  20378  decpmatid  20394  monmatcollpw  20403  mp2pm2mplem4  20433  chmatval  20453  chfacffsupp  20480  ptcmplem2  21667  ptcmplem3  21668  iccpnfhmeo  22552  xrhmeo  22553  phtpycc  22598  pcovalg  22620  pcohtpylem  22627  ovolunlem1a  23071  ovolunlem1  23072  ovolicc1  23091  ioorval  23148  mbfmax  23222  i1f1lem  23262  itg11  23264  itg1addlem3  23271  i1fres  23278  itg1climres  23287  mbfi1fseqlem4  23291  mbfi1fseqlem6  23293  mbfi1flimlem  23295  mbfi1flim  23296  itg2uba  23316  itg2splitlem  23321  itg2monolem1  23323  itg2gt0  23333  itg2cnlem1  23334  i1fibl  23380  itgeqa  23386  itgcn  23415  ditgex  23422  dvexp3  23545  ply1nzb  23686  ig1pval  23736  elply2  23756  dvply1  23843  aareccl  23885  dvtaylp  23928  pserdvlem2  23986  abelthlem9  23998  logtayl  24206  cxpval  24210  leibpilem2  24468  leibpi  24469  lgamgulmlem4  24558  lgamgulmlem5  24559  igamval  24573  vmaval  24639  vmaf  24645  muval  24658  prmorcht  24704  pclogsum  24740  dchrinvcl  24778  dchrptlem2  24790  bposlem5  24813  lgsval  24826  lgsfval  24827  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  gausslemma2dlem1  24891  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  padicval  25106  padicabv  25119  ostth1  25122  axlowdimlem15  25636  axlowdim  25641  vtxval  25677  iedgval  25678  clwlkisclwwlklem2a2  26308  psgnfzto1stlem  29181  xrge0iifcv  29308  xrge0iifhom  29311  ddeval1  29624  ddeval0  29625  mrsubcv  30661  mrsubrn  30664  dfrdg2  30945  finxpreclem2  32403  finxpreclem5  32408  poimirlem2  32581  poimirlem24  32603  mblfinlem2  32617  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  fdc  32711  renegclALT  33267  cdleme50f  34848  cdlemk40  35223  cdlemk56  35277  dihval  35539  dihf11lem  35573  mapdhval  36031  hdmap1vallem  36105  flcidc  36763  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem4  37362  fourierdlem29  39029  fourierdlem56  39055  fourierswlem  39123  fouriersw  39124  nnfoctbdjlem  39348  isomenndlem  39420  hoidmvval  39467  hspmbl  39519  crctcsh1wlkn0lem2  41014  crctcsh1wlkn0lem3  41015  clwlkclwwlklem2a2  41202  linc0scn0  42006  linc1  42008  lincext2  42038  blenval  42163