Theorem ifex 4429

Description: Conditional operator existence. (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 4427	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 2081  Vcvv 3437  ifcif 4381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-if 4382

This theorem is referenced by:  opex  5248  fnoe  7986  oev  7990  unxpdomlem1  8568  unxpdomlem2  8569  unxpdomlem3  8570  cantnflem1d  8997  cantnflem1  8998  iunfictbso  9386  fin23lem12  9599  axcc2lem  9704  ttukeylem3  9779  pwfseqlem2  9927  pwfseqlem3  9928  xnegex  12451  xaddval  12466  xmulval  12468  seqf1olem1  13259  expval  13281  bcval  13514  ccatlen  13773  ccatvalfn  13779  ccatalpha  13791  swrdval  13841  swrd00  13842  swrd0  13856  cshfn  13988  cshnz  13990  ofccat  14163  sgnval  14281  fsumser  14920  isumless  15033  rpnnen2lem1  15400  ruclem1  15417  sadcp1  15637  smupp1  15662  gcdval  15678  eucalgval2  15754  lcmval  15765  pcval  16010  pcmpt  16057  prmreclem2  16082  prmreclem5  16085  ramub1lem2  16192  ramcl  16194  acsfn  16759  gsumvalx  17709  mulgfval  17983  mulgfvalALT  17984  mulgval  17985  mulgfn  17986  odval  18393  odf  18396  gexval  18433  frgpup3lem  18630  dprdfeq0  18861  dmdprdsplitlem  18876  abvtrivd  19301  psrlidm  19871  psrridm  19872  mvrval2  19890  mplmonmul  19932  mplmon2  19960  coe1tmmul2fv  20129  coe1pwmulfv  20131  xrsdsval  20271  uvcvval  20612  mat1comp  20733  mat1ov  20741  matsc  20743  mat1dimid  20767  dmatmulcl  20793  scmatscmiddistr  20801  scmatscm  20806  mdetunilem9  20913  minmar1eval  20942  symgmatr01  20947  m2cpm  21033  m2cpminvid2lem  21046  decpmatid  21062  monmatcollpw  21071  mp2pm2mplem4  21101  chmatval  21121  chfacffsupp  21148  ptcmplem2  22345  ptcmplem3  22346  iccpnfhmeo  23232  xrhmeo  23233  phtpycc  23278  pcovalg  23299  pcohtpylem  23306  ovolunlem1a  23780  ovolunlem1  23781  ovolicc1  23800  ioorval  23858  mbfmax  23933  i1f1lem  23973  itg11  23975  itg1addlem3  23982  i1fres  23989  itg1climres  23998  mbfi1fseqlem4  24002  mbfi1fseqlem6  24004  mbfi1flimlem  24006  mbfi1flim  24007  itg2uba  24027  itg2splitlem  24032  itg2monolem1  24034  itg2gt0  24044  itg2cnlem1  24045  i1fibl  24091  itgeqa  24097  itgcn  24126  ditgex  24133  dvexp3  24258  ply1nzb  24399  ig1pval  24449  elply2  24469  dvply1  24556  aareccl  24598  dvtaylp  24641  pserdvlem2  24699  abelthlem9  24711  logtayl  24924  cxpval  24928  leibpilem2  25201  leibpi  25202  lgamgulmlem4  25291  lgamgulmlem5  25292  igamval  25306  vmaval  25372  vmaf  25378  muval  25391  prmorcht  25437  pclogsum  25473  dchrinvcl  25511  dchrptlem2  25523  bposlem5  25546  lgsval  25559  lgsfval  25560  lgsdir  25590  lgsdilem2  25591  lgsdi  25592  lgsne0  25593  gausslemma2dlem1  25624  pntrlog2bndlem4  25838  pntrlog2bndlem5  25839  padicval  25875  padicabv  25888  ostth1  25891  axlowdimlem15  26425  axlowdim  26430  vtxval  26468  iedgval  26469  crctcshwlkn0lem2  27276  crctcshwlkn0lem3  27277  clwlkclwwlklem2a2  27458  psgnfzto1stlem  30664  xrge0iifcv  30794  xrge0iifhom  30797  ddeval1  31110  ddeval0  31111  mrsubcv  32366  mrsubrn  32369  dfrdg2  32650  finxpreclem2  34221  finxpreclem5  34226  poimirlem2  34444  poimirlem24  34466  mblfinlem2  34480  itg2addnclem  34493  itg2addnclem2  34494  itg2addnclem3  34495  itg2addnc  34496  ftc1anclem5  34521  ftc1anclem7  34523  ftc1anclem8  34524  ftc1anc  34525  fdc  34571  renegclALT  35649  cdleme50f  37228  cdlemk40  37603  cdlemk56  37657  dihval  37918  dihf11lem  37952  mapdhval  38410  hdmap1vallem  38483  flcidc  39278  clsk1indlem2  39896  clsk1indlem3  39897  clsk1indlem4  39898  limsup10exlem  41614  fourierdlem29  41983  fourierdlem56  42009  fourierswlem  42077  fouriersw  42078  nnfoctbdjlem  42299  isomenndlem  42374  hoidmvval  42421  hspmbl  42473  linc0scn0  43978  linc1  43980  lincext2  44010  blenval  44132