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 2104  Vcvv 3437  ifcif 4465

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4466

This theorem is referenced by:  opex  5392  fnoe  8371  oev  8375  unxpdomlem1  9071  unxpdomlem2  9072  unxpdomlem3  9073  cantnflem1d  9490  cantnflem1  9491  ssttrcl  9517  ttrcltr  9518  ttrclselem2  9528  iunfictbso  9916  fin23lem12  10133  axcc2lem  10238  ttukeylem3  10313  pwfseqlem2  10461  pwfseqlem3  10462  xnegex  12988  xaddval  13003  xmulval  13005  seqf1olem1  13808  expval  13830  bcval  14064  ccatlen  14323  ccatlenOLD  14324  ccatvalfn  14331  ccatalpha  14343  swrdval  14401  swrd00  14402  swrd0  14416  cshfn  14548  cshnz  14550  ofccat  14725  sgnval  14844  fsumser  15487  isumless  15602  rpnnen2lem1  15968  ruclem1  15985  sadcp1  16207  smupp1  16232  gcdval  16248  eucalgval2  16331  lcmval  16342  pcval  16590  pcmpt  16638  prmreclem2  16663  prmreclem5  16666  ramub1lem2  16773  ramcl  16775  acsfn  17413  gsumvalx  18405  mulgfval  18747  mulgfvalALT  18748  mulgval  18749  mulgfn  18750  odval  19187  odf  19190  gexval  19228  frgpup3lem  19428  dprdfeq0  19670  dmdprdsplitlem  19685  abvtrivd  20145  xrsdsval  20687  uvcvval  21038  psrlidm  21217  psrridm  21218  mvrval2  21236  mplmonmul  21282  mplmon2  21314  coe1tmmul2fv  21494  coe1pwmulfv  21496  mat1comp  21634  mat1ov  21642  matsc  21644  mat1dimid  21668  dmatmulcl  21694  scmatscmiddistr  21702  scmatscm  21707  mdetunilem9  21814  minmar1eval  21843  symgmatr01  21848  m2cpm  21935  m2cpminvid2lem  21948  decpmatid  21964  monmatcollpw  21973  mp2pm2mplem4  22003  chmatval  22023  chfacffsupp  22050  ptcmplem2  23249  ptcmplem3  23250  iccpnfhmeo  24153  xrhmeo  24154  phtpycc  24199  pcovalg  24220  pcohtpylem  24227  ovolunlem1a  24705  ovolunlem1  24706  ovolicc1  24725  ioorval  24783  mbfmax  24858  i1f1lem  24898  itg11  24900  itg1addlem3  24907  i1fres  24915  itg1climres  24924  mbfi1fseqlem4  24928  mbfi1fseqlem6  24930  mbfi1flimlem  24932  mbfi1flim  24933  itg2uba  24953  itg2splitlem  24958  itg2monolem1  24960  itg2gt0  24970  itg2cnlem1  24971  i1fibl  25017  itgeqa  25023  itgcn  25054  ditgex  25061  dvexp3  25187  ply1nzb  25332  ig1pval  25382  elply2  25402  dvply1  25489  aareccl  25531  dvtaylp  25574  pserdvlem2  25632  abelthlem9  25644  logtayl  25860  cxpval  25864  leibpilem2  26136  leibpi  26137  lgamgulmlem4  26226  lgamgulmlem5  26227  igamval  26241  vmaval  26307  vmaf  26313  muval  26326  prmorcht  26372  pclogsum  26408  dchrinvcl  26446  dchrptlem2  26458  bposlem5  26481  lgsval  26494  lgsfval  26495  lgsdir  26525  lgsdilem2  26526  lgsdi  26527  lgsne0  26528  gausslemma2dlem1  26559  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  padicval  26810  padicabv  26823  ostth1  26826  axlowdimlem15  27369  axlowdim  27374  vtxval  27415  iedgval  27416  crctcshwlkn0lem2  28221  crctcshwlkn0lem3  28222  clwlkclwwlklem2a2  28402  psgnfzto1stlem  31412  xrge0iifcv  31929  xrge0iifhom  31932  ddeval1  32247  ddeval0  32248  mrsubcv  33517  mrsubrn  33520  dfrdg2  33816  finxpreclem2  35605  finxpreclem5  35610  poimirlem2  35823  poimirlem24  35845  mblfinlem2  35859  itg2addnclem  35872  itg2addnclem2  35873  itg2addnclem3  35874  itg2addnc  35875  ftc1anclem5  35898  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902  fdc  35947  renegclALT  37019  cdleme50f  38598  cdlemk40  38973  cdlemk56  39027  dihval  39288  dihf11lem  39322  mapdhval  39780  hdmap1vallem  39853  evlsbagval  40312  fsuppind  40316  mhphf  40322  flcidc  41037  clsk1indlem2  41690  clsk1indlem3  41691  clsk1indlem4  41692  limsup10exlem  43362  fourierdlem29  43726  fourierdlem56  43752  fourierswlem  43820  fouriersw  43821  nnfoctbdjlem  44043  isomenndlem  44118  hoidmvval  44165  hspmbl  44217  linc0scn0  45822  linc1  45824  lincext2  45854  blenval  45975