Theorem ifex 4535

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ifcif 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  opex  5419  fnoe  8451  oev  8455  unxpdomlem1  9173  unxpdomlem2  9174  unxpdomlem3  9175  cantnflem1d  9617  cantnflem1  9618  ssttrcl  9644  ttrcltr  9645  ttrclselem2  9655  iunfictbso  10043  fin23lem12  10260  axcc2lem  10365  ttukeylem3  10440  pwfseqlem2  10588  pwfseqlem3  10589  xnegex  13144  xaddval  13159  xmulval  13161  seqf1olem1  13982  expval  14004  bcval  14245  ccatlen  14516  ccatvalfn  14522  ccatalpha  14534  swrdval  14584  swrd00  14585  swrd0  14599  cshfn  14731  cshnz  14733  ofccat  14911  sgnval  15030  fsumser  15672  isumless  15787  rpnnen2lem1  16158  ruclem1  16175  sadcp1  16401  smupp1  16426  gcdval  16442  eucalgval2  16527  lcmval  16538  pcval  16791  pcmpt  16839  prmreclem2  16864  prmreclem5  16867  ramub1lem2  16974  ramcl  16976  acsfn  17596  gsumvalx  18579  mulgfval  18977  mulgfvalALT  18978  mulgval  18979  mulgfn  18980  odval  19440  odf  19443  gexval  19484  frgpup3lem  19683  dprdfeq0  19930  dmdprdsplitlem  19945  abvtrivd  20717  xrsdsval  21303  uvcvval  21671  psrlidm  21847  psrridm  21848  psrascl  21864  mvrval2  21868  mplmonmul  21919  mplmon2  21944  psdmplcl  22025  coe1tmmul2fv  22140  coe1pwmulfv  22142  mat1comp  22303  mat1ov  22311  matsc  22313  mat1dimid  22337  dmatmulcl  22363  scmatscmiddistr  22371  scmatscm  22376  mdetunilem9  22483  minmar1eval  22512  symgmatr01  22517  m2cpm  22604  m2cpminvid2lem  22617  decpmatid  22633  monmatcollpw  22642  mp2pm2mplem4  22672  chmatval  22692  chfacffsupp  22719  ptcmplem2  23916  ptcmplem3  23917  iccpnfhmeo  24819  xrhmeo  24820  phtpycc  24866  pcovalg  24888  pcohtpylem  24895  ovolunlem1a  25373  ovolunlem1  25374  ovolicc1  25393  ioorval  25451  mbfmax  25526  i1f1lem  25566  itg11  25568  itg1addlem3  25575  i1fres  25582  itg1climres  25591  mbfi1fseqlem4  25595  mbfi1fseqlem6  25597  mbfi1flimlem  25599  mbfi1flim  25600  itg2uba  25620  itg2splitlem  25625  itg2monolem1  25627  itg2gt0  25637  itg2cnlem1  25638  i1fibl  25685  itgeqa  25691  itgcn  25722  ditgex  25729  dvexp3  25858  ply1nzb  26004  ig1pval  26057  elply2  26077  dvply1  26167  aareccl  26210  dvtaylp  26254  pserdvlem2  26314  abelthlem9  26326  logtayl  26545  cxpval  26549  leibpilem2  26827  leibpi  26828  lgamgulmlem4  26918  lgamgulmlem5  26919  igamval  26933  vmaval  26999  vmaf  27005  muval  27018  prmorcht  27064  pclogsum  27102  dchrinvcl  27140  dchrptlem2  27152  bposlem5  27175  lgsval  27188  lgsfval  27189  lgsdir  27219  lgsdilem2  27220  lgsdi  27221  lgsne0  27222  gausslemma2dlem1  27253  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  padicval  27504  padicabv  27517  ostth1  27520  expsval  28287  axlowdimlem15  28859  axlowdim  28864  vtxval  28903  iedgval  28904  crctcshwlkn0lem2  29714  crctcshwlkn0lem3  29715  clwlkclwwlklem2a2  29895  psgnfzto1stlem  33030  xrge0iifcv  33897  xrge0iifhom  33900  ddeval1  34197  ddeval0  34198  mrsubcv  35470  mrsubrn  35473  dfrdg2  35756  finxpreclem2  37351  finxpreclem5  37356  poimirlem2  37589  poimirlem24  37611  mblfinlem2  37625  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  itg2addnc  37641  ftc1anclem5  37664  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  fdc  37712  renegclALT  38929  cdleme50f  40509  cdlemk40  40884  cdlemk56  40938  dihval  41199  dihf11lem  41233  mapdhval  41691  hdmap1vallem  41764  readvrec  42323  evlsbagval  42527  fsuppind  42551  flcidc  43132  cantnfub  43283  cantnfresb  43286  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  limsup10exlem  45743  fourierdlem29  46107  fourierdlem56  46133  fourierswlem  46201  fouriersw  46202  nnfoctbdjlem  46426  isomenndlem  46501  hoidmvval  46548  hspmbl  46600  linc0scn0  48385  linc1  48387  lincext2  48417  blenval  48533  discsubclem  49025  discsubc  49026  iinfconstbas  49028  oppffn  49086  oppfvalg  49088