Theorem ifex 4156

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

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifexg  4157  opex  4932  fnoe  7590  oev  7594  unxpdomlem1  8164  unxpdomlem2  8165  unxpdomlem3  8166  cantnflem1d  8585  cantnflem1  8586  iunfictbso  8937  fin23lem12  9153  axcc2lem  9258  ttukeylem3  9333  pwfseqlem2  9481  pwfseqlem3  9482  xnegex  12039  xaddval  12054  xmulval  12056  seqf1olem1  12840  expval  12862  bcval  13091  ccatlen  13360  ccatvalfn  13365  ccatalpha  13375  swrdval  13417  swrd00  13418  swrd0  13434  cshfn  13536  cshnz  13538  ofccat  13708  sgnval  13828  fsumser  14461  isumless  14577  rpnnen2lem1  14943  ruclem1  14960  sadcp1  15177  smupp1  15202  gcdval  15218  eucalgval2  15294  lcmval  15305  pcval  15549  pcmpt  15596  prmreclem2  15621  prmreclem5  15624  ramub1lem2  15731  ramcl  15733  acsfn  16320  gsumvalx  17270  mulgfval  17542  mulgval  17543  mulgfn  17544  odval  17953  odf  17956  gexval  17993  frgpup3lem  18190  dprdfeq0  18421  dmdprdsplitlem  18436  abvtrivd  18840  psrlidm  19403  psrridm  19404  mvrval2  19422  mplmonmul  19464  mplmon2  19493  coe1tmmul2fv  19648  coe1pwmulfv  19650  xrsdsval  19790  uvcvval  20125  mat1comp  20246  mat1ov  20254  matsc  20256  mat1dimid  20280  dmatmulcl  20306  scmatscmiddistr  20314  scmatscm  20319  mdetunilem9  20426  minmar1eval  20455  symgmatr01  20460  m2cpm  20546  m2cpminvid2lem  20559  decpmatid  20575  monmatcollpw  20584  mp2pm2mplem4  20614  chmatval  20634  chfacffsupp  20661  ptcmplem2  21857  ptcmplem3  21858  iccpnfhmeo  22744  xrhmeo  22745  phtpycc  22790  pcovalg  22812  pcohtpylem  22819  ovolunlem1a  23264  ovolunlem1  23265  ovolicc1  23284  ioorval  23342  mbfmax  23416  i1f1lem  23456  itg11  23458  itg1addlem3  23465  i1fres  23472  itg1climres  23481  mbfi1fseqlem4  23485  mbfi1fseqlem6  23487  mbfi1flimlem  23489  mbfi1flim  23490  itg2uba  23510  itg2splitlem  23515  itg2monolem1  23517  itg2gt0  23527  itg2cnlem1  23528  i1fibl  23574  itgeqa  23580  itgcn  23609  ditgex  23616  dvexp3  23741  ply1nzb  23882  ig1pval  23932  elply2  23952  dvply1  24039  aareccl  24081  dvtaylp  24124  pserdvlem2  24182  abelthlem9  24194  logtayl  24406  cxpval  24410  leibpilem2  24668  leibpi  24669  lgamgulmlem4  24758  lgamgulmlem5  24759  igamval  24773  vmaval  24839  vmaf  24845  muval  24858  prmorcht  24904  pclogsum  24940  dchrinvcl  24978  dchrptlem2  24990  bposlem5  25013  lgsval  25026  lgsfval  25027  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  gausslemma2dlem1  25091  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  padicval  25306  padicabv  25319  ostth1  25322  axlowdimlem15  25836  axlowdim  25841  vtxval  25878  iedgval  25879  vtxvalOLD  25880  iedgvalOLD  25881  crctcshwlkn0lem2  26703  crctcshwlkn0lem3  26704  clwlkclwwlklem2a2  26894  psgnfzto1stlem  29850  xrge0iifcv  29980  xrge0iifhom  29983  ddeval1  30297  ddeval0  30298  mrsubcv  31407  mrsubrn  31410  dfrdg2  31701  finxpreclem2  33227  finxpreclem5  33232  poimirlem2  33411  poimirlem24  33433  mblfinlem2  33447  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  fdc  33541  renegclALT  34249  cdleme50f  35830  cdlemk40  36205  cdlemk56  36259  dihval  36521  dihf11lem  36555  mapdhval  37013  hdmap1vallem  37087  flcidc  37744  clsk1indlem2  38340  clsk1indlem3  38341  clsk1indlem4  38342  limsup10exlem  40004  fourierdlem29  40353  fourierdlem56  40379  fourierswlem  40447  fouriersw  40448  nnfoctbdjlem  40672  isomenndlem  40744  hoidmvval  40791  hspmbl  40843  linc0scn0  42212  linc1  42214  lincext2  42244  blenval  42365