Theorem ifex 4533

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  opexOLD  5440  fnoe  8497  oev  8501  unxpdomlem1  9226  unxpdomlem2  9227  unxpdomlem3  9228  cantnflem1d  9667  cantnflem1  9668  ssttrcl  9694  ttrcltr  9695  ttrclselem2  9705  iunfictbso  10117  fin23lem12  10333  axcc2lem  10438  ttukeylem3  10513  pwfseqlem2  10668  pwfseqlem3  10669  xnegex  13260  xaddval  13275  xmulval  13277  seqf1olem1  14105  expval  14127  bcval  14368  ccatlen  14640  ccatvalfn  14646  ccatalpha  14660  swrdval  14711  swrd00  14712  swrd0  14728  cshfn  14861  cshnz  14863  ofccat  15042  sgnval  15161  sgndm  15169  fsumser  15816  isumless  15934  rpnnen2lem1  16302  ruclem1  16319  sadcp1  16545  smupp1  16570  gcdval  16586  eucalgval2  16671  lcmval  16682  pcval  16936  pcmpt  16984  prmreclem2  17009  prmreclem5  17012  ramub1lem2  17119  ramcl  17121  acsfn  17747  gsumvalx  18778  mulgfval  19192  mulgfvalALT  19193  mulgval  19194  mulgfn  19195  odval  19661  odf  19664  gexval  19705  frgpup3lem  19904  dprdfeq0  20151  dmdprdsplitlem  20166  abvtrivd  20998  xrsdsval  21624  uvcvval  21999  psrlidm  22176  psrridm  22177  psrascl  22193  mvrval2  22197  mplmonmul  22252  mplmon2  22277  psdmplcl  22390  coe1tmmul2fv  22504  coe1pwmulfv  22506  mat1comp  22662  mat1ov  22670  matsc  22672  mat1dimid  22696  dmatmulcl  22722  scmatscmiddistr  22730  scmatscm  22735  mdetunilem9  22842  minmar1eval  22871  symgmatr01  22876  m2cpm  22966  m2cpminvid2lem  22979  decpmatid  22995  monmatcollpw  23004  mp2pm2mplem4  23034  chmatval  23054  chfacffsupp  23081  ptcmplem2  24279  ptcmplem3  24280  iccpnfhmeo  25173  xrhmeo  25174  phtpycc  25219  pcovalg  25240  pcohtpylem  25247  ovolunlem1a  25724  ovolunlem1  25725  ovolicc1  25744  ioorval  25802  mbfmax  25877  i1f1lem  25917  itg11  25919  itg1addlem3  25926  i1fres  25933  itg1climres  25942  mbfi1fseqlem4  25946  mbfi1fseqlem6  25948  mbfi1flimlem  25950  mbfi1flim  25951  itg2uba  25971  itg2splitlem  25976  itg2monolem1  25978  itg2gt0  25988  itg2cnlem1  25989  i1fibl  26035  itgeqa  26041  itgcn  26072  ditgex  26079  dvexp3  26205  ply1nzb  26348  ig1pval  26401  elply2  26421  dvply1  26514  aareccl  26562  dvtaylp  26606  pserdvlem2  26664  abelthlem9  26676  logtayl  26897  cxpval  26901  leibpilem2  27178  leibpi  27179  lgamgulmlem4  27268  lgamgulmlem5  27269  igamval  27283  vmaval  27349  vmaf  27355  muval  27368  prmorcht  27414  pclogsum  27451  dchrinvcl  27489  dchrptlem2  27501  bposlem5  27524  lgsval  27537  lgsfval  27538  lgsdir  27568  lgsdilem2  27569  lgsdi  27570  lgsne0  27571  gausslemma2dlem1  27602  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  padicval  27853  padicabv  27866  ostth1  27869  expsval  28690  axlowdimlem15  29413  axlowdim  29418  vtxval  29457  iedgval  29458  crctcshwlkn0lem2  30279  crctcshwlkn0lem3  30280  clwlkclwwlklem2a2  30463  psgnfzto1stlem  33540  psrmonmul  34060  xrge0iifcv  34444  xrge0iifhom  34447  ddeval1  34745  ddeval0  34746  vonf1oonfo  35712  mrsubcv  36089  mrsubrn  36092  dfrdg2  36372  finxpreclem2  38144  finxpreclem5  38149  poimirlem2  38371  poimirlem24  38393  mblfinlem2  38407  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  itg2addnc  38423  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  fdc  38495  renegclALT  39836  cdleme50f  41415  cdlemk40  41790  cdlemk56  41844  dihval  42105  dihf11lem  42139  mapdhval  42597  hdmap1vallem  42670  readvrec  43237  evlsbagval  43432  fsuppind  43436  flcidc  44011  cantnfub  44162  cantnfresb  44165  clsk1indlem2  44882  clsk1indlem3  44883  clsk1indlem4  44884  limsup10exlem  46600  fourierdlem29  46964  fourierdlem56  46990  fourierswlem  47058  fouriersw  47059  nnfoctbdjlem  47283  isomenndlem  47358  hoidmvval  47405  hspmbl  47457  linc0scn0  49353  linc1  49355  lincext2  49385  blenval  49501  discsubclem  49989  discsubc  49990  iinfconstbas  49992  oppffn  50050  oppfvalg  50052  veronesevrowd  50812