Theorem ifex 4556

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464  ifcif 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  opex  5444  fnoe  8527  oev  8531  unxpdomlem1  9263  unxpdomlem2  9264  unxpdomlem3  9265  cantnflem1d  9707  cantnflem1  9708  ssttrcl  9734  ttrcltr  9735  ttrclselem2  9745  iunfictbso  10133  fin23lem12  10350  axcc2lem  10455  ttukeylem3  10530  pwfseqlem2  10678  pwfseqlem3  10679  xnegex  13229  xaddval  13244  xmulval  13246  seqf1olem1  14064  expval  14086  bcval  14327  ccatlen  14598  ccatvalfn  14604  ccatalpha  14616  swrdval  14666  swrd00  14667  swrd0  14681  cshfn  14813  cshnz  14815  ofccat  14993  sgnval  15112  fsumser  15751  isumless  15866  rpnnen2lem1  16237  ruclem1  16254  sadcp1  16479  smupp1  16504  gcdval  16520  eucalgval2  16605  lcmval  16616  pcval  16869  pcmpt  16917  prmreclem2  16942  prmreclem5  16945  ramub1lem2  17052  ramcl  17054  acsfn  17676  gsumvalx  18659  mulgfval  19057  mulgfvalALT  19058  mulgval  19059  mulgfn  19060  odval  19520  odf  19523  gexval  19564  frgpup3lem  19763  dprdfeq0  20010  dmdprdsplitlem  20025  abvtrivd  20797  xrsdsval  21383  uvcvval  21751  psrlidm  21927  psrridm  21928  psrascl  21944  mvrval2  21948  mplmonmul  21999  mplmon2  22024  psdmplcl  22105  coe1tmmul2fv  22220  coe1pwmulfv  22222  mat1comp  22383  mat1ov  22391  matsc  22393  mat1dimid  22417  dmatmulcl  22443  scmatscmiddistr  22451  scmatscm  22456  mdetunilem9  22563  minmar1eval  22592  symgmatr01  22597  m2cpm  22684  m2cpminvid2lem  22697  decpmatid  22713  monmatcollpw  22722  mp2pm2mplem4  22752  chmatval  22772  chfacffsupp  22799  ptcmplem2  23996  ptcmplem3  23997  iccpnfhmeo  24899  xrhmeo  24900  phtpycc  24946  pcovalg  24968  pcohtpylem  24975  ovolunlem1a  25454  ovolunlem1  25455  ovolicc1  25474  ioorval  25532  mbfmax  25607  i1f1lem  25647  itg11  25649  itg1addlem3  25656  i1fres  25663  itg1climres  25672  mbfi1fseqlem4  25676  mbfi1fseqlem6  25678  mbfi1flimlem  25680  mbfi1flim  25681  itg2uba  25701  itg2splitlem  25706  itg2monolem1  25708  itg2gt0  25718  itg2cnlem1  25719  i1fibl  25766  itgeqa  25772  itgcn  25803  ditgex  25810  dvexp3  25939  ply1nzb  26085  ig1pval  26138  elply2  26158  dvply1  26248  aareccl  26291  dvtaylp  26335  pserdvlem2  26395  abelthlem9  26407  logtayl  26626  cxpval  26630  leibpilem2  26908  leibpi  26909  lgamgulmlem4  26999  lgamgulmlem5  27000  igamval  27014  vmaval  27080  vmaf  27086  muval  27099  prmorcht  27145  pclogsum  27183  dchrinvcl  27221  dchrptlem2  27233  bposlem5  27256  lgsval  27269  lgsfval  27270  lgsdir  27300  lgsdilem2  27301  lgsdi  27302  lgsne0  27303  gausslemma2dlem1  27334  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  padicval  27585  padicabv  27598  ostth1  27601  expsval  28368  axlowdimlem15  28940  axlowdim  28945  vtxval  28984  iedgval  28985  crctcshwlkn0lem2  29798  crctcshwlkn0lem3  29799  clwlkclwwlklem2a2  29979  psgnfzto1stlem  33116  xrge0iifcv  33970  xrge0iifhom  33973  ddeval1  34270  ddeval0  34271  mrsubcv  35537  mrsubrn  35540  dfrdg2  35818  finxpreclem2  37413  finxpreclem5  37418  poimirlem2  37651  poimirlem24  37673  mblfinlem2  37687  itg2addnclem  37700  itg2addnclem2  37701  itg2addnclem3  37702  itg2addnc  37703  ftc1anclem5  37726  ftc1anclem7  37728  ftc1anclem8  37729  ftc1anc  37730  fdc  37774  renegclALT  38986  cdleme50f  40566  cdlemk40  40941  cdlemk56  40995  dihval  41256  dihf11lem  41290  mapdhval  41748  hdmap1vallem  41821  readvrec  42380  evlsbagval  42564  fsuppind  42588  flcidc  43169  cantnfub  43320  cantnfresb  43323  clsk1indlem2  44041  clsk1indlem3  44042  clsk1indlem4  44043  limsup10exlem  45781  fourierdlem29  46145  fourierdlem56  46171  fourierswlem  46239  fouriersw  46240  nnfoctbdjlem  46464  isomenndlem  46539  hoidmvval  46586  hspmbl  46638  linc0scn0  48379  linc1  48381  lincext2  48411  blenval  48531  discsubclem  49010  discsubc  49011  iinfconstbas  49013  oppfvalg  49054  oppfrcl  49056