Theorem ifex 4580

Description: Existence of the conditional operator (inference form). (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 4577	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 2098  Vcvv 3461  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531

This theorem is referenced by:  opex  5466  fnoe  8531  oev  8535  unxpdomlem1  9275  unxpdomlem2  9276  unxpdomlem3  9277  cantnflem1d  9713  cantnflem1  9714  ssttrcl  9740  ttrcltr  9741  ttrclselem2  9751  iunfictbso  10139  fin23lem12  10356  axcc2lem  10461  ttukeylem3  10536  pwfseqlem2  10684  pwfseqlem3  10685  xnegex  13222  xaddval  13237  xmulval  13239  seqf1olem1  14042  expval  14064  bcval  14299  ccatlen  14561  ccatvalfn  14567  ccatalpha  14579  swrdval  14629  swrd00  14630  swrd0  14644  cshfn  14776  cshnz  14778  ofccat  14952  sgnval  15071  fsumser  15712  isumless  15827  rpnnen2lem1  16194  ruclem1  16211  sadcp1  16433  smupp1  16458  gcdval  16474  eucalgval2  16555  lcmval  16566  pcval  16816  pcmpt  16864  prmreclem2  16889  prmreclem5  16892  ramub1lem2  16999  ramcl  17001  acsfn  17642  gsumvalx  18639  mulgfval  19033  mulgfvalALT  19034  mulgval  19035  mulgfn  19036  odval  19501  odf  19504  gexval  19545  frgpup3lem  19744  dprdfeq0  19991  dmdprdsplitlem  20006  abvtrivd  20732  xrsdsval  21360  uvcvval  21737  psrlidm  21924  psrridm  21925  psrascl  21941  mvrval2  21945  mplmonmul  21996  mplmon2  22027  psdmplcl  22109  coe1tmmul2fv  22222  coe1pwmulfv  22224  mat1comp  22386  mat1ov  22394  matsc  22396  mat1dimid  22420  dmatmulcl  22446  scmatscmiddistr  22454  scmatscm  22459  mdetunilem9  22566  minmar1eval  22595  symgmatr01  22600  m2cpm  22687  m2cpminvid2lem  22700  decpmatid  22716  monmatcollpw  22725  mp2pm2mplem4  22755  chmatval  22775  chfacffsupp  22802  ptcmplem2  24001  ptcmplem3  24002  iccpnfhmeo  24914  xrhmeo  24915  phtpycc  24961  pcovalg  24983  pcohtpylem  24990  ovolunlem1a  25469  ovolunlem1  25470  ovolicc1  25489  ioorval  25547  mbfmax  25622  i1f1lem  25662  itg11  25664  itg1addlem3  25671  i1fres  25679  itg1climres  25688  mbfi1fseqlem4  25692  mbfi1fseqlem6  25694  mbfi1flimlem  25696  mbfi1flim  25697  itg2uba  25717  itg2splitlem  25722  itg2monolem1  25724  itg2gt0  25734  itg2cnlem1  25735  i1fibl  25781  itgeqa  25787  itgcn  25818  ditgex  25825  dvexp3  25954  ply1nzb  26103  ig1pval  26155  elply2  26175  dvply1  26263  aareccl  26306  dvtaylp  26350  pserdvlem2  26410  abelthlem9  26422  logtayl  26639  cxpval  26643  leibpilem2  26918  leibpi  26919  lgamgulmlem4  27009  lgamgulmlem5  27010  igamval  27024  vmaval  27090  vmaf  27096  muval  27109  prmorcht  27155  pclogsum  27193  dchrinvcl  27231  dchrptlem2  27243  bposlem5  27266  lgsval  27279  lgsfval  27280  lgsdir  27310  lgsdilem2  27311  lgsdi  27312  lgsne0  27313  gausslemma2dlem1  27344  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  padicval  27595  padicabv  27608  ostth1  27611  axlowdimlem15  28839  axlowdim  28844  vtxval  28885  iedgval  28886  crctcshwlkn0lem2  29694  crctcshwlkn0lem3  29695  clwlkclwwlklem2a2  29875  psgnfzto1stlem  32913  xrge0iifcv  33666  xrge0iifhom  33669  ddeval1  33984  ddeval0  33985  mrsubcv  35251  mrsubrn  35254  dfrdg2  35522  finxpreclem2  37000  finxpreclem5  37005  poimirlem2  37226  poimirlem24  37248  mblfinlem2  37262  itg2addnclem  37275  itg2addnclem2  37276  itg2addnclem3  37277  itg2addnc  37278  ftc1anclem5  37301  ftc1anclem7  37303  ftc1anclem8  37304  ftc1anc  37305  fdc  37349  renegclALT  38565  cdleme50f  40145  cdlemk40  40520  cdlemk56  40574  dihval  40835  dihf11lem  40869  mapdhval  41327  hdmap1vallem  41400  evlsbagval  41934  fsuppind  41958  flcidc  42740  cantnfub  42892  cantnfresb  42895  clsk1indlem2  43614  clsk1indlem3  43615  clsk1indlem4  43616  limsup10exlem  45298  fourierdlem29  45662  fourierdlem56  45688  fourierswlem  45756  fouriersw  45757  nnfoctbdjlem  45981  isomenndlem  46056  hoidmvval  46103  hspmbl  46155  linc0scn0  47677  linc1  47679  lincext2  47709  blenval  47830