Theorem ifex 4598

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  opex  5484  fnoe  8566  oev  8570  unxpdomlem1  9313  unxpdomlem2  9314  unxpdomlem3  9315  cantnflem1d  9757  cantnflem1  9758  ssttrcl  9784  ttrcltr  9785  ttrclselem2  9795  iunfictbso  10183  fin23lem12  10400  axcc2lem  10505  ttukeylem3  10580  pwfseqlem2  10728  pwfseqlem3  10729  xnegex  13270  xaddval  13285  xmulval  13287  seqf1olem1  14092  expval  14114  bcval  14353  ccatlen  14623  ccatvalfn  14629  ccatalpha  14641  swrdval  14691  swrd00  14692  swrd0  14706  cshfn  14838  cshnz  14840  ofccat  15018  sgnval  15137  fsumser  15778  isumless  15893  rpnnen2lem1  16262  ruclem1  16279  sadcp1  16501  smupp1  16526  gcdval  16542  eucalgval2  16628  lcmval  16639  pcval  16891  pcmpt  16939  prmreclem2  16964  prmreclem5  16967  ramub1lem2  17074  ramcl  17076  acsfn  17717  gsumvalx  18714  mulgfval  19109  mulgfvalALT  19110  mulgval  19111  mulgfn  19112  odval  19576  odf  19579  gexval  19620  frgpup3lem  19819  dprdfeq0  20066  dmdprdsplitlem  20081  abvtrivd  20855  xrsdsval  21451  uvcvval  21829  psrlidm  22005  psrridm  22006  psrascl  22022  mvrval2  22026  mplmonmul  22077  mplmon2  22108  psdmplcl  22189  coe1tmmul2fv  22302  coe1pwmulfv  22304  mat1comp  22467  mat1ov  22475  matsc  22477  mat1dimid  22501  dmatmulcl  22527  scmatscmiddistr  22535  scmatscm  22540  mdetunilem9  22647  minmar1eval  22676  symgmatr01  22681  m2cpm  22768  m2cpminvid2lem  22781  decpmatid  22797  monmatcollpw  22806  mp2pm2mplem4  22836  chmatval  22856  chfacffsupp  22883  ptcmplem2  24082  ptcmplem3  24083  iccpnfhmeo  24995  xrhmeo  24996  phtpycc  25042  pcovalg  25064  pcohtpylem  25071  ovolunlem1a  25550  ovolunlem1  25551  ovolicc1  25570  ioorval  25628  mbfmax  25703  i1f1lem  25743  itg11  25745  itg1addlem3  25752  i1fres  25760  itg1climres  25769  mbfi1fseqlem4  25773  mbfi1fseqlem6  25775  mbfi1flimlem  25777  mbfi1flim  25778  itg2uba  25798  itg2splitlem  25803  itg2monolem1  25805  itg2gt0  25815  itg2cnlem1  25816  i1fibl  25863  itgeqa  25869  itgcn  25900  ditgex  25907  dvexp3  26036  ply1nzb  26182  ig1pval  26235  elply2  26255  dvply1  26343  aareccl  26386  dvtaylp  26430  pserdvlem2  26490  abelthlem9  26502  logtayl  26720  cxpval  26724  leibpilem2  27002  leibpi  27003  lgamgulmlem4  27093  lgamgulmlem5  27094  igamval  27108  vmaval  27174  vmaf  27180  muval  27193  prmorcht  27239  pclogsum  27277  dchrinvcl  27315  dchrptlem2  27327  bposlem5  27350  lgsval  27363  lgsfval  27364  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  gausslemma2dlem1  27428  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  padicval  27679  padicabv  27692  ostth1  27695  expsval  28426  axlowdimlem15  28989  axlowdim  28994  vtxval  29035  iedgval  29036  crctcshwlkn0lem2  29844  crctcshwlkn0lem3  29845  clwlkclwwlklem2a2  30025  psgnfzto1stlem  33093  xrge0iifcv  33880  xrge0iifhom  33883  ddeval1  34198  ddeval0  34199  mrsubcv  35478  mrsubrn  35481  dfrdg2  35759  finxpreclem2  37356  finxpreclem5  37361  poimirlem2  37582  poimirlem24  37604  mblfinlem2  37618  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  itg2addnc  37634  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  fdc  37705  renegclALT  38919  cdleme50f  40499  cdlemk40  40874  cdlemk56  40928  dihval  41189  dihf11lem  41223  mapdhval  41681  hdmap1vallem  41754  evlsbagval  42521  fsuppind  42545  flcidc  43131  cantnfub  43283  cantnfresb  43286  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  limsup10exlem  45693  fourierdlem29  46057  fourierdlem56  46083  fourierswlem  46151  fouriersw  46152  nnfoctbdjlem  46376  isomenndlem  46451  hoidmvval  46498  hspmbl  46550  linc0scn0  48152  linc1  48154  lincext2  48184  blenval  48305