Theorem ifex 4293

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

Syntax hints:   ∈ wcel 2155  Vcvv 3350  ifcif 4245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-if 4246

This theorem is referenced by:  opex  5090  fnoe  7797  oev  7801  unxpdomlem1  8373  unxpdomlem2  8374  unxpdomlem3  8375  cantnflem1d  8802  cantnflem1  8803  iunfictbso  9190  fin23lem12  9408  axcc2lem  9513  ttukeylem3  9588  pwfseqlem2  9736  pwfseqlem3  9737  xnegex  12244  xaddval  12259  xmulval  12261  seqf1olem1  13050  expval  13072  bcval  13298  ccatlen  13549  ccatvalfn  13555  ccatalpha  13567  swrdval  13621  swrd00  13622  swrd0  13639  cshfn  13819  cshfnOLD  13820  cshnz  13822  cshnzOLD  13823  ofccat  13998  sgnval  14116  fsumser  14749  isumless  14864  rpnnen2lem1  15228  ruclem1  15245  sadcp1  15461  smupp1  15486  gcdval  15502  eucalgval2  15578  lcmval  15589  pcval  15831  pcmpt  15878  prmreclem2  15903  prmreclem5  15906  ramub1lem2  16013  ramcl  16015  acsfn  16588  gsumvalx  17539  mulgfval  17812  mulgval  17813  mulgfn  17814  odval  18220  odf  18223  gexval  18260  frgpup3lem  18459  dprdfeq0  18691  dmdprdsplitlem  18706  abvtrivd  19112  psrlidm  19680  psrridm  19681  mvrval2  19699  mplmonmul  19741  mplmon2  19769  coe1tmmul2fv  19924  coe1pwmulfv  19926  xrsdsval  20066  uvcvval  20404  mat1comp  20525  mat1ov  20534  matsc  20536  mat1dimid  20560  dmatmulcl  20586  scmatscmiddistr  20594  scmatscm  20599  mdetunilem9  20706  minmar1eval  20735  symgmatr01  20741  m2cpm  20828  m2cpminvid2lem  20841  decpmatid  20857  monmatcollpw  20866  mp2pm2mplem4  20896  chmatval  20916  chfacffsupp  20943  ptcmplem2  22139  ptcmplem3  22140  iccpnfhmeo  23026  xrhmeo  23027  phtpycc  23072  pcovalg  23093  pcohtpylem  23100  ovolunlem1a  23557  ovolunlem1  23558  ovolicc1  23577  ioorval  23635  mbfmax  23710  i1f1lem  23750  itg11  23752  itg1addlem3  23759  i1fres  23766  itg1climres  23775  mbfi1fseqlem4  23779  mbfi1fseqlem6  23781  mbfi1flimlem  23783  mbfi1flim  23784  itg2uba  23804  itg2splitlem  23809  itg2monolem1  23811  itg2gt0  23821  itg2cnlem1  23822  i1fibl  23868  itgeqa  23874  itgcn  23903  ditgex  23910  dvexp3  24035  ply1nzb  24176  ig1pval  24226  elply2  24246  dvply1  24333  aareccl  24375  dvtaylp  24418  pserdvlem2  24476  abelthlem9  24488  logtayl  24700  cxpval  24704  leibpilem2  24962  leibpi  24963  lgamgulmlem4  25052  lgamgulmlem5  25053  igamval  25067  vmaval  25133  vmaf  25139  muval  25152  prmorcht  25198  pclogsum  25234  dchrinvcl  25272  dchrptlem2  25284  bposlem5  25307  lgsval  25320  lgsfval  25321  lgsdir  25351  lgsdilem2  25352  lgsdi  25353  lgsne0  25354  gausslemma2dlem1  25385  pntrlog2bndlem4  25563  pntrlog2bndlem5  25564  padicval  25600  padicabv  25613  ostth1  25616  axlowdimlem15  26130  axlowdim  26135  vtxval  26172  iedgval  26173  crctcshwlkn0lem2  26999  crctcshwlkn0lem3  27000  clwlkclwwlklem2a2  27223  psgnfzto1stlem  30300  xrge0iifcv  30430  xrge0iifhom  30433  ddeval1  30747  ddeval0  30748  mrsubcv  31858  mrsubrn  31861  dfrdg2  32147  finxpreclem2  33663  finxpreclem5  33668  poimirlem2  33838  poimirlem24  33860  mblfinlem2  33874  itg2addnclem  33887  itg2addnclem2  33888  itg2addnclem3  33889  itg2addnc  33890  ftc1anclem5  33915  ftc1anclem7  33917  ftc1anclem8  33918  ftc1anc  33919  fdc  33966  renegclALT  34922  cdleme50f  36501  cdlemk40  36876  cdlemk56  36930  dihval  37191  dihf11lem  37225  mapdhval  37683  hdmap1vallem  37756  flcidc  38424  clsk1indlem2  39017  clsk1indlem3  39018  clsk1indlem4  39019  limsup10exlem  40645  fourierdlem29  40993  fourierdlem56  41019  fourierswlem  41087  fouriersw  41088  nnfoctbdjlem  41312  isomenndlem  41387  hoidmvval  41434  hspmbl  41486  linc0scn0  42884  linc1  42886  lincext2  42916  blenval  43037