Theorem ifex 4530

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  opex  5412  fnoe  8437  oev  8441  unxpdomlem1  9156  unxpdomlem2  9157  unxpdomlem3  9158  cantnflem1d  9597  cantnflem1  9598  ssttrcl  9624  ttrcltr  9625  ttrclselem2  9635  iunfictbso  10024  fin23lem12  10241  axcc2lem  10346  ttukeylem3  10421  pwfseqlem2  10570  pwfseqlem3  10571  xnegex  13123  xaddval  13138  xmulval  13140  seqf1olem1  13964  expval  13986  bcval  14227  ccatlen  14498  ccatvalfn  14504  ccatalpha  14517  swrdval  14567  swrd00  14568  swrd0  14582  cshfn  14713  cshnz  14715  ofccat  14892  sgnval  15011  fsumser  15653  isumless  15768  rpnnen2lem1  16139  ruclem1  16156  sadcp1  16382  smupp1  16407  gcdval  16423  eucalgval2  16508  lcmval  16519  pcval  16772  pcmpt  16820  prmreclem2  16845  prmreclem5  16848  ramub1lem2  16955  ramcl  16957  acsfn  17582  gsumvalx  18601  mulgfval  18999  mulgfvalALT  19000  mulgval  19001  mulgfn  19002  odval  19463  odf  19466  gexval  19507  frgpup3lem  19706  dprdfeq0  19953  dmdprdsplitlem  19968  abvtrivd  20765  xrsdsval  21365  uvcvval  21741  psrlidm  21917  psrridm  21918  psrascl  21934  mvrval2  21938  mplmonmul  21991  mplmon2  22016  psdmplcl  22105  coe1tmmul2fv  22220  coe1pwmulfv  22222  mat1comp  22384  mat1ov  22392  matsc  22394  mat1dimid  22418  dmatmulcl  22444  scmatscmiddistr  22452  scmatscm  22457  mdetunilem9  22564  minmar1eval  22593  symgmatr01  22598  m2cpm  22685  m2cpminvid2lem  22698  decpmatid  22714  monmatcollpw  22723  mp2pm2mplem4  22753  chmatval  22773  chfacffsupp  22800  ptcmplem2  23997  ptcmplem3  23998  iccpnfhmeo  24899  xrhmeo  24900  phtpycc  24946  pcovalg  24968  pcohtpylem  24975  ovolunlem1a  25453  ovolunlem1  25454  ovolicc1  25473  ioorval  25531  mbfmax  25606  i1f1lem  25646  itg11  25648  itg1addlem3  25655  i1fres  25662  itg1climres  25671  mbfi1fseqlem4  25675  mbfi1fseqlem6  25677  mbfi1flimlem  25679  mbfi1flim  25680  itg2uba  25700  itg2splitlem  25705  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  i1fibl  25765  itgeqa  25771  itgcn  25802  ditgex  25809  dvexp3  25938  ply1nzb  26084  ig1pval  26137  elply2  26157  dvply1  26247  aareccl  26290  dvtaylp  26334  pserdvlem2  26394  abelthlem9  26406  logtayl  26625  cxpval  26629  leibpilem2  26907  leibpi  26908  lgamgulmlem4  26998  lgamgulmlem5  26999  igamval  27013  vmaval  27079  vmaf  27085  muval  27098  prmorcht  27144  pclogsum  27182  dchrinvcl  27220  dchrptlem2  27232  bposlem5  27255  lgsval  27268  lgsfval  27269  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  gausslemma2dlem1  27333  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  padicval  27584  padicabv  27597  ostth1  27600  expsval  28421  axlowdimlem15  29029  axlowdim  29034  vtxval  29073  iedgval  29074  crctcshwlkn0lem2  29884  crctcshwlkn0lem3  29885  clwlkclwwlklem2a2  30068  psgnfzto1stlem  33182  xrge0iifcv  34091  xrge0iifhom  34094  ddeval1  34391  ddeval0  34392  mrsubcv  35704  mrsubrn  35707  dfrdg2  35987  finxpreclem2  37595  finxpreclem5  37600  poimirlem2  37823  poimirlem24  37845  mblfinlem2  37859  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  itg2addnc  37875  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  fdc  37946  renegclALT  39223  cdleme50f  40802  cdlemk40  41177  cdlemk56  41231  dihval  41492  dihf11lem  41526  mapdhval  41984  hdmap1vallem  42057  readvrec  42617  evlsbagval  42812  fsuppind  42833  flcidc  43412  cantnfub  43563  cantnfresb  43566  clsk1indlem2  44283  clsk1indlem3  44284  clsk1indlem4  44285  limsup10exlem  46016  fourierdlem29  46380  fourierdlem56  46406  fourierswlem  46474  fouriersw  46475  nnfoctbdjlem  46699  isomenndlem  46774  hoidmvval  46821  hspmbl  46873  linc0scn0  48669  linc1  48671  lincext2  48701  blenval  48817  discsubclem  49308  discsubc  49309  iinfconstbas  49311  oppffn  49369  oppfvalg  49371