Theorem ifex 4515

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

Syntax hints:   ∈ wcel 2110  Vcvv 3431  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-if 4466

This theorem is referenced by:  opex  5383  fnoe  8325  oev  8329  unxpdomlem1  9005  unxpdomlem2  9006  unxpdomlem3  9007  cantnflem1d  9424  cantnflem1  9425  ssttrcl  9451  ttrcltr  9452  ttrclselem2  9462  iunfictbso  9871  fin23lem12  10088  axcc2lem  10193  ttukeylem3  10268  pwfseqlem2  10416  pwfseqlem3  10417  xnegex  12941  xaddval  12956  xmulval  12958  seqf1olem1  13760  expval  13782  bcval  14016  ccatlen  14276  ccatlenOLD  14277  ccatvalfn  14284  ccatalpha  14296  swrdval  14354  swrd00  14355  swrd0  14369  cshfn  14501  cshnz  14503  ofccat  14678  sgnval  14797  fsumser  15440  isumless  15555  rpnnen2lem1  15921  ruclem1  15938  sadcp1  16160  smupp1  16185  gcdval  16201  eucalgval2  16284  lcmval  16295  pcval  16543  pcmpt  16591  prmreclem2  16616  prmreclem5  16619  ramub1lem2  16726  ramcl  16728  acsfn  17366  gsumvalx  18358  mulgfval  18700  mulgfvalALT  18701  mulgval  18702  mulgfn  18703  odval  19140  odf  19143  gexval  19181  frgpup3lem  19381  dprdfeq0  19623  dmdprdsplitlem  19638  abvtrivd  20098  xrsdsval  20640  uvcvval  20991  psrlidm  21170  psrridm  21171  mvrval2  21189  mplmonmul  21235  mplmon2  21267  coe1tmmul2fv  21447  coe1pwmulfv  21449  mat1comp  21587  mat1ov  21595  matsc  21597  mat1dimid  21621  dmatmulcl  21647  scmatscmiddistr  21655  scmatscm  21660  mdetunilem9  21767  minmar1eval  21796  symgmatr01  21801  m2cpm  21888  m2cpminvid2lem  21901  decpmatid  21917  monmatcollpw  21926  mp2pm2mplem4  21956  chmatval  21976  chfacffsupp  22003  ptcmplem2  23202  ptcmplem3  23203  iccpnfhmeo  24106  xrhmeo  24107  phtpycc  24152  pcovalg  24173  pcohtpylem  24180  ovolunlem1a  24658  ovolunlem1  24659  ovolicc1  24678  ioorval  24736  mbfmax  24811  i1f1lem  24851  itg11  24853  itg1addlem3  24860  i1fres  24868  itg1climres  24877  mbfi1fseqlem4  24881  mbfi1fseqlem6  24883  mbfi1flimlem  24885  mbfi1flim  24886  itg2uba  24906  itg2splitlem  24911  itg2monolem1  24913  itg2gt0  24923  itg2cnlem1  24924  i1fibl  24970  itgeqa  24976  itgcn  25007  ditgex  25014  dvexp3  25140  ply1nzb  25285  ig1pval  25335  elply2  25355  dvply1  25442  aareccl  25484  dvtaylp  25527  pserdvlem2  25585  abelthlem9  25597  logtayl  25813  cxpval  25817  leibpilem2  26089  leibpi  26090  lgamgulmlem4  26179  lgamgulmlem5  26180  igamval  26194  vmaval  26260  vmaf  26266  muval  26279  prmorcht  26325  pclogsum  26361  dchrinvcl  26399  dchrptlem2  26411  bposlem5  26434  lgsval  26447  lgsfval  26448  lgsdir  26478  lgsdilem2  26479  lgsdi  26480  lgsne0  26481  gausslemma2dlem1  26512  pntrlog2bndlem4  26726  pntrlog2bndlem5  26727  padicval  26763  padicabv  26776  ostth1  26779  axlowdimlem15  27322  axlowdim  27327  vtxval  27368  iedgval  27369  crctcshwlkn0lem2  28172  crctcshwlkn0lem3  28173  clwlkclwwlklem2a2  28353  psgnfzto1stlem  31363  xrge0iifcv  31880  xrge0iifhom  31883  ddeval1  32198  ddeval0  32199  mrsubcv  33468  mrsubrn  33471  dfrdg2  33767  finxpreclem2  35557  finxpreclem5  35562  poimirlem2  35775  poimirlem24  35797  mblfinlem2  35811  itg2addnclem  35824  itg2addnclem2  35825  itg2addnclem3  35826  itg2addnc  35827  ftc1anclem5  35850  ftc1anclem7  35852  ftc1anclem8  35853  ftc1anc  35854  fdc  35899  renegclALT  36973  cdleme50f  38552  cdlemk40  38927  cdlemk56  38981  dihval  39242  dihf11lem  39276  mapdhval  39734  hdmap1vallem  39807  evlsbagval  40272  fsuppind  40276  mhphf  40282  flcidc  40996  clsk1indlem2  41622  clsk1indlem3  41623  clsk1indlem4  41624  limsup10exlem  43284  fourierdlem29  43648  fourierdlem56  43674  fourierswlem  43742  fouriersw  43743  nnfoctbdjlem  43964  isomenndlem  44039  hoidmvval  44086  hspmbl  44138  linc0scn0  45733  linc1  45735  lincext2  45765  blenval  45886