Theorem ifex 4517

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  opexOLD  5417  fnoe  8445  oev  8449  unxpdomlem1  9166  unxpdomlem2  9167  unxpdomlem3  9168  cantnflem1d  9609  cantnflem1  9610  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  iunfictbso  10036  fin23lem12  10253  axcc2lem  10358  ttukeylem3  10433  pwfseqlem2  10582  pwfseqlem3  10583  xnegex  13160  xaddval  13175  xmulval  13177  seqf1olem1  14003  expval  14025  bcval  14266  ccatlen  14537  ccatvalfn  14543  ccatalpha  14556  swrdval  14606  swrd00  14607  swrd0  14621  cshfn  14752  cshnz  14754  ofccat  14931  sgnval  15050  fsumser  15692  isumless  15810  rpnnen2lem1  16181  ruclem1  16198  sadcp1  16424  smupp1  16449  gcdval  16465  eucalgval2  16550  lcmval  16561  pcval  16815  pcmpt  16863  prmreclem2  16888  prmreclem5  16891  ramub1lem2  16998  ramcl  17000  acsfn  17625  gsumvalx  18644  mulgfval  19045  mulgfvalALT  19046  mulgval  19047  mulgfn  19048  odval  19509  odf  19512  gexval  19553  frgpup3lem  19752  dprdfeq0  19999  dmdprdsplitlem  20014  abvtrivd  20809  xrsdsval  21391  uvcvval  21766  psrlidm  21940  psrridm  21941  psrascl  21957  mvrval2  21961  mplmonmul  22014  mplmon2  22039  psdmplcl  22128  coe1tmmul2fv  22243  coe1pwmulfv  22245  mat1comp  22405  mat1ov  22413  matsc  22415  mat1dimid  22439  dmatmulcl  22465  scmatscmiddistr  22473  scmatscm  22478  mdetunilem9  22585  minmar1eval  22614  symgmatr01  22619  m2cpm  22706  m2cpminvid2lem  22719  decpmatid  22735  monmatcollpw  22744  mp2pm2mplem4  22774  chmatval  22794  chfacffsupp  22821  ptcmplem2  24018  ptcmplem3  24019  iccpnfhmeo  24912  xrhmeo  24913  phtpycc  24958  pcovalg  24979  pcohtpylem  24986  ovolunlem1a  25463  ovolunlem1  25464  ovolicc1  25483  ioorval  25541  mbfmax  25616  i1f1lem  25656  itg11  25658  itg1addlem3  25665  i1fres  25672  itg1climres  25681  mbfi1fseqlem4  25685  mbfi1fseqlem6  25687  mbfi1flimlem  25689  mbfi1flim  25690  itg2uba  25710  itg2splitlem  25715  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  i1fibl  25775  itgeqa  25781  itgcn  25812  ditgex  25819  dvexp3  25945  ply1nzb  26088  ig1pval  26141  elply2  26161  dvply1  26250  aareccl  26292  dvtaylp  26335  pserdvlem2  26393  abelthlem9  26405  logtayl  26624  cxpval  26628  leibpilem2  26905  leibpi  26906  lgamgulmlem4  26995  lgamgulmlem5  26996  igamval  27010  vmaval  27076  vmaf  27082  muval  27095  prmorcht  27141  pclogsum  27178  dchrinvcl  27216  dchrptlem2  27228  bposlem5  27251  lgsval  27264  lgsfval  27265  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  gausslemma2dlem1  27329  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  padicval  27580  padicabv  27593  ostth1  27596  expsval  28417  axlowdimlem15  29025  axlowdim  29030  vtxval  29069  iedgval  29070  crctcshwlkn0lem2  29879  crctcshwlkn0lem3  29880  clwlkclwwlklem2a2  30063  psgnfzto1stlem  33161  psrmonmul  33694  xrge0iifcv  34078  xrge0iifhom  34081  ddeval1  34378  ddeval0  34379  mrsubcv  35692  mrsubrn  35695  dfrdg2  35975  finxpreclem2  37706  finxpreclem5  37711  poimirlem2  37943  poimirlem24  37965  mblfinlem2  37979  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  itg2addnc  37995  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  fdc  38066  renegclALT  39409  cdleme50f  40988  cdlemk40  41363  cdlemk56  41417  dihval  41678  dihf11lem  41712  mapdhval  42170  hdmap1vallem  42243  readvrec  42794  evlsbagval  43002  fsuppind  43023  flcidc  43598  cantnfub  43749  cantnfresb  43752  clsk1indlem2  44469  clsk1indlem3  44470  clsk1indlem4  44471  limsup10exlem  46200  fourierdlem29  46564  fourierdlem56  46590  fourierswlem  46658  fouriersw  46659  nnfoctbdjlem  46883  isomenndlem  46958  hoidmvval  47005  hspmbl  47057  linc0scn0  48899  linc1  48901  lincext2  48931  blenval  49047  discsubclem  49538  discsubc  49539  iinfconstbas  49541  oppffn  49599  oppfvalg  49601