Theorem ifex 4579

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  opex  5465  fnoe  8510  oev  8514  unxpdomlem1  9250  unxpdomlem2  9251  unxpdomlem3  9252  cantnflem1d  9683  cantnflem1  9684  ssttrcl  9710  ttrcltr  9711  ttrclselem2  9721  iunfictbso  10109  fin23lem12  10326  axcc2lem  10431  ttukeylem3  10506  pwfseqlem2  10654  pwfseqlem3  10655  xnegex  13187  xaddval  13202  xmulval  13204  seqf1olem1  14007  expval  14029  bcval  14264  ccatlen  14525  ccatvalfn  14531  ccatalpha  14543  swrdval  14593  swrd00  14594  swrd0  14608  cshfn  14740  cshnz  14742  ofccat  14916  sgnval  15035  fsumser  15676  isumless  15791  rpnnen2lem1  16157  ruclem1  16174  sadcp1  16396  smupp1  16421  gcdval  16437  eucalgval2  16518  lcmval  16529  pcval  16777  pcmpt  16825  prmreclem2  16850  prmreclem5  16853  ramub1lem2  16960  ramcl  16962  acsfn  17603  gsumvalx  18595  mulgfval  18952  mulgfvalALT  18953  mulgval  18954  mulgfn  18955  odval  19402  odf  19405  gexval  19446  frgpup3lem  19645  dprdfeq0  19892  dmdprdsplitlem  19907  abvtrivd  20448  xrsdsval  20989  uvcvval  21341  psrlidm  21523  psrridm  21524  mvrval2  21542  mplmonmul  21591  mplmon2  21622  coe1tmmul2fv  21800  coe1pwmulfv  21802  mat1comp  21942  mat1ov  21950  matsc  21952  mat1dimid  21976  dmatmulcl  22002  scmatscmiddistr  22010  scmatscm  22015  mdetunilem9  22122  minmar1eval  22151  symgmatr01  22156  m2cpm  22243  m2cpminvid2lem  22256  decpmatid  22272  monmatcollpw  22281  mp2pm2mplem4  22311  chmatval  22331  chfacffsupp  22358  ptcmplem2  23557  ptcmplem3  23558  iccpnfhmeo  24461  xrhmeo  24462  phtpycc  24507  pcovalg  24528  pcohtpylem  24535  ovolunlem1a  25013  ovolunlem1  25014  ovolicc1  25033  ioorval  25091  mbfmax  25166  i1f1lem  25206  itg11  25208  itg1addlem3  25215  i1fres  25223  itg1climres  25232  mbfi1fseqlem4  25236  mbfi1fseqlem6  25238  mbfi1flimlem  25240  mbfi1flim  25241  itg2uba  25261  itg2splitlem  25266  itg2monolem1  25268  itg2gt0  25278  itg2cnlem1  25279  i1fibl  25325  itgeqa  25331  itgcn  25362  ditgex  25369  dvexp3  25495  ply1nzb  25640  ig1pval  25690  elply2  25710  dvply1  25797  aareccl  25839  dvtaylp  25882  pserdvlem2  25940  abelthlem9  25952  logtayl  26168  cxpval  26172  leibpilem2  26446  leibpi  26447  lgamgulmlem4  26536  lgamgulmlem5  26537  igamval  26551  vmaval  26617  vmaf  26623  muval  26636  prmorcht  26682  pclogsum  26718  dchrinvcl  26756  dchrptlem2  26768  bposlem5  26791  lgsval  26804  lgsfval  26805  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  gausslemma2dlem1  26869  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  padicval  27120  padicabv  27133  ostth1  27136  axlowdimlem15  28214  axlowdim  28219  vtxval  28260  iedgval  28261  crctcshwlkn0lem2  29065  crctcshwlkn0lem3  29066  clwlkclwwlklem2a2  29246  psgnfzto1stlem  32259  xrge0iifcv  32914  xrge0iifhom  32917  ddeval1  33232  ddeval0  33233  mrsubcv  34501  mrsubrn  34504  dfrdg2  34767  finxpreclem2  36271  finxpreclem5  36276  poimirlem2  36490  poimirlem24  36512  mblfinlem2  36526  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  itg2addnc  36542  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  fdc  36613  renegclALT  37833  cdleme50f  39413  cdlemk40  39788  cdlemk56  39842  dihval  40103  dihf11lem  40137  mapdhval  40595  hdmap1vallem  40668  evlsbagval  41138  fsuppind  41162  flcidc  41916  cantnfub  42071  cantnfresb  42074  clsk1indlem2  42793  clsk1indlem3  42794  clsk1indlem4  42795  limsup10exlem  44488  fourierdlem29  44852  fourierdlem56  44878  fourierswlem  44946  fouriersw  44947  nnfoctbdjlem  45171  isomenndlem  45246  hoidmvval  45293  hspmbl  45345  linc0scn0  47104  linc1  47106  lincext2  47136  blenval  47257