Theorem ifex 4515

Description: Conditional operator existence. (Contributed by NM, 2-Sep-2004.)

Hypotheses

Ref	Expression
ifex.1	⊢ 𝐴 ∈ V
ifex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ifex	⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Proof of Theorem ifex

Step	Hyp	Ref	Expression
1		ifex.1	. 2 ⊢ 𝐴 ∈ V
2		ifex.2	. 2 ⊢ 𝐵 ∈ V
3	1, 2	ifcli 4513	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-if 4468

This theorem is referenced by:  opex  5356  fnoe  8135  oev  8139  unxpdomlem1  8722  unxpdomlem2  8723  unxpdomlem3  8724  cantnflem1d  9151  cantnflem1  9152  iunfictbso  9540  fin23lem12  9753  axcc2lem  9858  ttukeylem3  9933  pwfseqlem2  10081  pwfseqlem3  10082  xnegex  12602  xaddval  12617  xmulval  12619  seqf1olem1  13410  expval  13432  bcval  13665  ccatlen  13927  ccatlenOLD  13928  ccatvalfn  13935  ccatalpha  13947  swrdval  14005  swrd00  14006  swrd0  14020  cshfn  14152  cshnz  14154  ofccat  14329  sgnval  14447  fsumser  15087  isumless  15200  rpnnen2lem1  15567  ruclem1  15584  sadcp1  15804  smupp1  15829  gcdval  15845  eucalgval2  15925  lcmval  15936  pcval  16181  pcmpt  16228  prmreclem2  16253  prmreclem5  16256  ramub1lem2  16363  ramcl  16365  acsfn  16930  gsumvalx  17886  mulgfval  18226  mulgfvalALT  18227  mulgval  18228  mulgfn  18229  odval  18662  odf  18665  gexval  18703  frgpup3lem  18903  dprdfeq0  19144  dmdprdsplitlem  19159  abvtrivd  19611  psrlidm  20183  psrridm  20184  mvrval2  20202  mplmonmul  20245  mplmon2  20273  coe1tmmul2fv  20446  coe1pwmulfv  20448  xrsdsval  20589  uvcvval  20930  mat1comp  21049  mat1ov  21057  matsc  21059  mat1dimid  21083  dmatmulcl  21109  scmatscmiddistr  21117  scmatscm  21122  mdetunilem9  21229  minmar1eval  21258  symgmatr01  21263  m2cpm  21349  m2cpminvid2lem  21362  decpmatid  21378  monmatcollpw  21387  mp2pm2mplem4  21417  chmatval  21437  chfacffsupp  21464  ptcmplem2  22661  ptcmplem3  22662  iccpnfhmeo  23549  xrhmeo  23550  phtpycc  23595  pcovalg  23616  pcohtpylem  23623  ovolunlem1a  24097  ovolunlem1  24098  ovolicc1  24117  ioorval  24175  mbfmax  24250  i1f1lem  24290  itg11  24292  itg1addlem3  24299  i1fres  24306  itg1climres  24315  mbfi1fseqlem4  24319  mbfi1fseqlem6  24321  mbfi1flimlem  24323  mbfi1flim  24324  itg2uba  24344  itg2splitlem  24349  itg2monolem1  24351  itg2gt0  24361  itg2cnlem1  24362  i1fibl  24408  itgeqa  24414  itgcn  24443  ditgex  24450  dvexp3  24575  ply1nzb  24716  ig1pval  24766  elply2  24786  dvply1  24873  aareccl  24915  dvtaylp  24958  pserdvlem2  25016  abelthlem9  25028  logtayl  25243  cxpval  25247  leibpilem2  25519  leibpi  25520  lgamgulmlem4  25609  lgamgulmlem5  25610  igamval  25624  vmaval  25690  vmaf  25696  muval  25709  prmorcht  25755  pclogsum  25791  dchrinvcl  25829  dchrptlem2  25841  bposlem5  25864  lgsval  25877  lgsfval  25878  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  gausslemma2dlem1  25942  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  padicval  26193  padicabv  26206  ostth1  26209  axlowdimlem15  26742  axlowdim  26747  vtxval  26785  iedgval  26786  crctcshwlkn0lem2  27589  crctcshwlkn0lem3  27590  clwlkclwwlklem2a2  27771  psgnfzto1stlem  30742  xrge0iifcv  31177  xrge0iifhom  31180  ddeval1  31493  ddeval0  31494  mrsubcv  32757  mrsubrn  32760  dfrdg2  33040  finxpreclem2  34674  finxpreclem5  34679  poimirlem2  34909  poimirlem24  34931  mblfinlem2  34945  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  itg2addnc  34961  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  fdc  35035  renegclALT  36114  cdleme50f  37693  cdlemk40  38068  cdlemk56  38122  dihval  38383  dihf11lem  38417  mapdhval  38875  hdmap1vallem  38948  flcidc  39823  clsk1indlem2  40441  clsk1indlem3  40442  clsk1indlem4  40443  limsup10exlem  42102  fourierdlem29  42470  fourierdlem56  42496  fourierswlem  42564  fouriersw  42565  nnfoctbdjlem  42786  isomenndlem  42861  hoidmvval  42908  hspmbl  42960  linc0scn0  44527  linc1  44529  lincext2  44559  blenval  44680