Theorem ifex 4517

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 4515	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ifcif 4469

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 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  opex  5358  fnoe  8137  oev  8141  unxpdomlem1  8724  unxpdomlem2  8725  unxpdomlem3  8726  cantnflem1d  9153  cantnflem1  9154  iunfictbso  9542  fin23lem12  9755  axcc2lem  9860  ttukeylem3  9935  pwfseqlem2  10083  pwfseqlem3  10084  xnegex  12604  xaddval  12619  xmulval  12621  seqf1olem1  13412  expval  13434  bcval  13667  ccatlen  13929  ccatlenOLD  13930  ccatvalfn  13937  ccatalpha  13949  swrdval  14007  swrd00  14008  swrd0  14022  cshfn  14154  cshnz  14156  ofccat  14331  sgnval  14449  fsumser  15089  isumless  15202  rpnnen2lem1  15569  ruclem1  15586  sadcp1  15806  smupp1  15831  gcdval  15847  eucalgval2  15927  lcmval  15938  pcval  16183  pcmpt  16230  prmreclem2  16255  prmreclem5  16258  ramub1lem2  16365  ramcl  16367  acsfn  16932  gsumvalx  17888  mulgfval  18228  mulgfvalALT  18229  mulgval  18230  mulgfn  18231  odval  18664  odf  18667  gexval  18705  frgpup3lem  18905  dprdfeq0  19146  dmdprdsplitlem  19161  abvtrivd  19613  psrlidm  20185  psrridm  20186  mvrval2  20204  mplmonmul  20247  mplmon2  20275  coe1tmmul2fv  20448  coe1pwmulfv  20450  xrsdsval  20591  uvcvval  20932  mat1comp  21051  mat1ov  21059  matsc  21061  mat1dimid  21085  dmatmulcl  21111  scmatscmiddistr  21119  scmatscm  21124  mdetunilem9  21231  minmar1eval  21260  symgmatr01  21265  m2cpm  21351  m2cpminvid2lem  21364  decpmatid  21380  monmatcollpw  21389  mp2pm2mplem4  21419  chmatval  21439  chfacffsupp  21466  ptcmplem2  22663  ptcmplem3  22664  iccpnfhmeo  23551  xrhmeo  23552  phtpycc  23597  pcovalg  23618  pcohtpylem  23625  ovolunlem1a  24099  ovolunlem1  24100  ovolicc1  24119  ioorval  24177  mbfmax  24252  i1f1lem  24292  itg11  24294  itg1addlem3  24301  i1fres  24308  itg1climres  24317  mbfi1fseqlem4  24321  mbfi1fseqlem6  24323  mbfi1flimlem  24325  mbfi1flim  24326  itg2uba  24346  itg2splitlem  24351  itg2monolem1  24353  itg2gt0  24363  itg2cnlem1  24364  i1fibl  24410  itgeqa  24416  itgcn  24445  ditgex  24452  dvexp3  24577  ply1nzb  24718  ig1pval  24768  elply2  24788  dvply1  24875  aareccl  24917  dvtaylp  24960  pserdvlem2  25018  abelthlem9  25030  logtayl  25245  cxpval  25249  leibpilem2  25521  leibpi  25522  lgamgulmlem4  25611  lgamgulmlem5  25612  igamval  25626  vmaval  25692  vmaf  25698  muval  25711  prmorcht  25757  pclogsum  25793  dchrinvcl  25831  dchrptlem2  25843  bposlem5  25866  lgsval  25879  lgsfval  25880  lgsdir  25910  lgsdilem2  25911  lgsdi  25912  lgsne0  25913  gausslemma2dlem1  25944  pntrlog2bndlem4  26158  pntrlog2bndlem5  26159  padicval  26195  padicabv  26208  ostth1  26211  axlowdimlem15  26744  axlowdim  26749  vtxval  26787  iedgval  26788  crctcshwlkn0lem2  27591  crctcshwlkn0lem3  27592  clwlkclwwlklem2a2  27773  psgnfzto1stlem  30744  xrge0iifcv  31179  xrge0iifhom  31182  ddeval1  31495  ddeval0  31496  mrsubcv  32759  mrsubrn  32762  dfrdg2  33042  finxpreclem2  34673  finxpreclem5  34678  poimirlem2  34896  poimirlem24  34918  mblfinlem2  34932  itg2addnclem  34945  itg2addnclem2  34946  itg2addnclem3  34947  itg2addnc  34948  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  fdc  35022  renegclALT  36101  cdleme50f  37680  cdlemk40  38055  cdlemk56  38109  dihval  38370  dihf11lem  38404  mapdhval  38862  hdmap1vallem  38935  flcidc  39781  clsk1indlem2  40399  clsk1indlem3  40400  clsk1indlem4  40401  limsup10exlem  42060  fourierdlem29  42428  fourierdlem56  42454  fourierswlem  42522  fouriersw  42523  nnfoctbdjlem  42744  isomenndlem  42819  hoidmvval  42866  hspmbl  42918  linc0scn0  44485  linc1  44487  lincext2  44517  blenval  44638