Theorem ifex 4558

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

Syntax hints:   ∈ wcel 2107  Vcvv 3464  ifcif 4507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-if 4508

This theorem is referenced by:  opex  5451  fnoe  8531  oev  8535  unxpdomlem1  9269  unxpdomlem2  9270  unxpdomlem3  9271  cantnflem1d  9711  cantnflem1  9712  ssttrcl  9738  ttrcltr  9739  ttrclselem2  9749  iunfictbso  10137  fin23lem12  10354  axcc2lem  10459  ttukeylem3  10534  pwfseqlem2  10682  pwfseqlem3  10683  xnegex  13233  xaddval  13248  xmulval  13250  seqf1olem1  14065  expval  14087  bcval  14326  ccatlen  14596  ccatvalfn  14602  ccatalpha  14614  swrdval  14664  swrd00  14665  swrd0  14679  cshfn  14811  cshnz  14813  ofccat  14991  sgnval  15110  fsumser  15749  isumless  15864  rpnnen2lem1  16233  ruclem1  16250  sadcp1  16475  smupp1  16500  gcdval  16516  eucalgval2  16601  lcmval  16612  pcval  16865  pcmpt  16913  prmreclem2  16938  prmreclem5  16941  ramub1lem2  17048  ramcl  17050  acsfn  17678  gsumvalx  18663  mulgfval  19061  mulgfvalALT  19062  mulgval  19063  mulgfn  19064  odval  19525  odf  19528  gexval  19569  frgpup3lem  19768  dprdfeq0  20015  dmdprdsplitlem  20030  abvtrivd  20806  xrsdsval  21395  uvcvval  21773  psrlidm  21949  psrridm  21950  psrascl  21966  mvrval2  21970  mplmonmul  22021  mplmon2  22052  psdmplcl  22133  coe1tmmul2fv  22248  coe1pwmulfv  22250  mat1comp  22413  mat1ov  22421  matsc  22423  mat1dimid  22447  dmatmulcl  22473  scmatscmiddistr  22481  scmatscm  22486  mdetunilem9  22593  minmar1eval  22622  symgmatr01  22627  m2cpm  22714  m2cpminvid2lem  22727  decpmatid  22743  monmatcollpw  22752  mp2pm2mplem4  22782  chmatval  22802  chfacffsupp  22829  ptcmplem2  24026  ptcmplem3  24027  iccpnfhmeo  24931  xrhmeo  24932  phtpycc  24978  pcovalg  25000  pcohtpylem  25007  ovolunlem1a  25486  ovolunlem1  25487  ovolicc1  25506  ioorval  25564  mbfmax  25639  i1f1lem  25679  itg11  25681  itg1addlem3  25688  i1fres  25695  itg1climres  25704  mbfi1fseqlem4  25708  mbfi1fseqlem6  25710  mbfi1flimlem  25712  mbfi1flim  25713  itg2uba  25733  itg2splitlem  25738  itg2monolem1  25740  itg2gt0  25750  itg2cnlem1  25751  i1fibl  25798  itgeqa  25804  itgcn  25835  ditgex  25842  dvexp3  25971  ply1nzb  26117  ig1pval  26170  elply2  26190  dvply1  26280  aareccl  26323  dvtaylp  26367  pserdvlem2  26427  abelthlem9  26439  logtayl  26657  cxpval  26661  leibpilem2  26939  leibpi  26940  lgamgulmlem4  27030  lgamgulmlem5  27031  igamval  27045  vmaval  27111  vmaf  27117  muval  27130  prmorcht  27176  pclogsum  27214  dchrinvcl  27252  dchrptlem2  27264  bposlem5  27287  lgsval  27300  lgsfval  27301  lgsdir  27331  lgsdilem2  27332  lgsdi  27333  lgsne0  27334  gausslemma2dlem1  27365  pntrlog2bndlem4  27579  pntrlog2bndlem5  27580  padicval  27616  padicabv  27629  ostth1  27632  expsval  28363  axlowdimlem15  28920  axlowdim  28925  vtxval  28964  iedgval  28965  crctcshwlkn0lem2  29778  crctcshwlkn0lem3  29779  clwlkclwwlklem2a2  29959  psgnfzto1stlem  33066  xrge0iifcv  33874  xrge0iifhom  33877  ddeval1  34176  ddeval0  34177  mrsubcv  35456  mrsubrn  35459  dfrdg2  35737  finxpreclem2  37332  finxpreclem5  37337  poimirlem2  37570  poimirlem24  37592  mblfinlem2  37606  itg2addnclem  37619  itg2addnclem2  37620  itg2addnclem3  37621  itg2addnc  37622  ftc1anclem5  37645  ftc1anclem7  37647  ftc1anclem8  37648  ftc1anc  37649  fdc  37693  renegclALT  38905  cdleme50f  40485  cdlemk40  40860  cdlemk56  40914  dihval  41175  dihf11lem  41209  mapdhval  41667  hdmap1vallem  41740  readvrec  42337  evlsbagval  42521  fsuppind  42545  flcidc  43127  cantnfub  43279  cantnfresb  43282  clsk1indlem2  44000  clsk1indlem3  44001  clsk1indlem4  44002  limsup10exlem  45732  fourierdlem29  46096  fourierdlem56  46122  fourierswlem  46190  fouriersw  46191  nnfoctbdjlem  46415  isomenndlem  46490  hoidmvval  46537  hspmbl  46589  linc0scn0  48286  linc1  48288  lincext2  48318  blenval  48438