Theorem ifex 4581

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

Syntax hints:   ∈ wcel 2106  Vcvv 3478  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  opex  5475  fnoe  8547  oev  8551  unxpdomlem1  9284  unxpdomlem2  9285  unxpdomlem3  9286  cantnflem1d  9726  cantnflem1  9727  ssttrcl  9753  ttrcltr  9754  ttrclselem2  9764  iunfictbso  10152  fin23lem12  10369  axcc2lem  10474  ttukeylem3  10549  pwfseqlem2  10697  pwfseqlem3  10698  xnegex  13247  xaddval  13262  xmulval  13264  seqf1olem1  14079  expval  14101  bcval  14340  ccatlen  14610  ccatvalfn  14616  ccatalpha  14628  swrdval  14678  swrd00  14679  swrd0  14693  cshfn  14825  cshnz  14827  ofccat  15005  sgnval  15124  fsumser  15763  isumless  15878  rpnnen2lem1  16247  ruclem1  16264  sadcp1  16489  smupp1  16514  gcdval  16530  eucalgval2  16615  lcmval  16626  pcval  16878  pcmpt  16926  prmreclem2  16951  prmreclem5  16954  ramub1lem2  17061  ramcl  17063  acsfn  17704  gsumvalx  18702  mulgfval  19100  mulgfvalALT  19101  mulgval  19102  mulgfn  19103  odval  19567  odf  19570  gexval  19611  frgpup3lem  19810  dprdfeq0  20057  dmdprdsplitlem  20072  abvtrivd  20850  xrsdsval  21446  uvcvval  21824  psrlidm  22000  psrridm  22001  psrascl  22017  mvrval2  22021  mplmonmul  22072  mplmon2  22103  psdmplcl  22184  coe1tmmul2fv  22297  coe1pwmulfv  22299  mat1comp  22462  mat1ov  22470  matsc  22472  mat1dimid  22496  dmatmulcl  22522  scmatscmiddistr  22530  scmatscm  22535  mdetunilem9  22642  minmar1eval  22671  symgmatr01  22676  m2cpm  22763  m2cpminvid2lem  22776  decpmatid  22792  monmatcollpw  22801  mp2pm2mplem4  22831  chmatval  22851  chfacffsupp  22878  ptcmplem2  24077  ptcmplem3  24078  iccpnfhmeo  24990  xrhmeo  24991  phtpycc  25037  pcovalg  25059  pcohtpylem  25066  ovolunlem1a  25545  ovolunlem1  25546  ovolicc1  25565  ioorval  25623  mbfmax  25698  i1f1lem  25738  itg11  25740  itg1addlem3  25747  i1fres  25755  itg1climres  25764  mbfi1fseqlem4  25768  mbfi1fseqlem6  25770  mbfi1flimlem  25772  mbfi1flim  25773  itg2uba  25793  itg2splitlem  25798  itg2monolem1  25800  itg2gt0  25810  itg2cnlem1  25811  i1fibl  25858  itgeqa  25864  itgcn  25895  ditgex  25902  dvexp3  26031  ply1nzb  26177  ig1pval  26230  elply2  26250  dvply1  26340  aareccl  26383  dvtaylp  26427  pserdvlem2  26487  abelthlem9  26499  logtayl  26717  cxpval  26721  leibpilem2  26999  leibpi  27000  lgamgulmlem4  27090  lgamgulmlem5  27091  igamval  27105  vmaval  27171  vmaf  27177  muval  27190  prmorcht  27236  pclogsum  27274  dchrinvcl  27312  dchrptlem2  27324  bposlem5  27347  lgsval  27360  lgsfval  27361  lgsdir  27391  lgsdilem2  27392  lgsdi  27393  lgsne0  27394  gausslemma2dlem1  27425  pntrlog2bndlem4  27639  pntrlog2bndlem5  27640  padicval  27676  padicabv  27689  ostth1  27692  expsval  28423  axlowdimlem15  28986  axlowdim  28991  vtxval  29032  iedgval  29033  crctcshwlkn0lem2  29841  crctcshwlkn0lem3  29842  clwlkclwwlklem2a2  30022  psgnfzto1stlem  33103  xrge0iifcv  33895  xrge0iifhom  33898  ddeval1  34215  ddeval0  34216  mrsubcv  35495  mrsubrn  35498  dfrdg2  35777  finxpreclem2  37373  finxpreclem5  37378  poimirlem2  37609  poimirlem24  37631  mblfinlem2  37645  itg2addnclem  37658  itg2addnclem2  37659  itg2addnclem3  37660  itg2addnc  37661  ftc1anclem5  37684  ftc1anclem7  37686  ftc1anclem8  37687  ftc1anc  37688  fdc  37732  renegclALT  38945  cdleme50f  40525  cdlemk40  40900  cdlemk56  40954  dihval  41215  dihf11lem  41249  mapdhval  41707  hdmap1vallem  41780  readvrec  42371  evlsbagval  42553  fsuppind  42577  flcidc  43159  cantnfub  43311  cantnfresb  43314  clsk1indlem2  44032  clsk1indlem3  44033  clsk1indlem4  44034  limsup10exlem  45728  fourierdlem29  46092  fourierdlem56  46118  fourierswlem  46186  fouriersw  46187  nnfoctbdjlem  46411  isomenndlem  46486  hoidmvval  46533  hspmbl  46585  linc0scn0  48269  linc1  48271  lincext2  48301  blenval  48421