Theorem ifex 4532

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  opexOLD  5432  fnoe  8522  oev  8526  unxpdomlem1  9251  unxpdomlem2  9252  unxpdomlem3  9253  cantnflem1d  9693  cantnflem1  9694  ssttrcl  9720  ttrcltr  9721  ttrclselem2  9731  iunfictbso  10197  fin23lem12  10413  axcc2lem  10518  ttukeylem3  10593  pwfseqlem2  10748  pwfseqlem3  10749  xnegex  13342  xaddval  13357  xmulval  13359  seqf1olem1  14188  expval  14210  bcval  14452  ccatlen  14724  ccatvalfn  14730  ccatalpha  14744  swrdval  14796  swrd00  14797  swrd0  14813  cshfn  14946  cshnz  14948  ofccat  15128  sgnval  15247  sgndm  15255  fsumser  15902  isumless  16020  rpnnen2lem1  16388  ruclem1  16405  sadcp1  16631  smupp1  16656  gcdval  16672  eucalgval2  16762  lcmval  16773  pcval  17028  pcmpt  17076  prmreclem2  17101  prmreclem5  17104  ramub1lem2  17211  ramcl  17213  acsfn  17839  gsumvalx  18871  mulgfval  19285  mulgfvalALT  19286  mulgval  19287  mulgfn  19288  odval  19754  odf  19757  gexval  19798  frgpup3lem  19997  dprdfeq0  20244  dmdprdsplitlem  20259  abvtrivd  21095  xrsdsval  21723  uvcvval  22098  psrlidm  22275  psrridm  22276  psrascl  22292  mvrval2  22296  mplmonmul  22351  mplmon2  22376  psdmplcl  22489  coe1tmmul2fv  22603  coe1pwmulfv  22605  mat1comp  22761  mat1ov  22769  matsc  22771  mat1dimid  22795  dmatmulcl  22821  scmatscmiddistr  22829  scmatscm  22834  mdetunilem9  22941  minmar1eval  22970  symgmatr01  22975  m2cpm  23065  m2cpminvid2lem  23078  decpmatid  23094  monmatcollpw  23103  mp2pm2mplem4  23133  chmatval  23153  chfacffsupp  23180  ptcmplem2  24378  ptcmplem3  24379  iccpnfhmeo  25272  xrhmeo  25273  phtpycc  25318  pcovalg  25339  pcohtpylem  25346  ovolunlem1a  25823  ovolunlem1  25824  ovolicc1  25843  ioorval  25901  mbfmax  25976  i1f1lem  26016  itg11  26018  itg1addlem3  26025  i1fres  26032  itg1climres  26041  mbfi1fseqlem4  26045  mbfi1fseqlem6  26047  mbfi1flimlem  26049  mbfi1flim  26050  itg2uba  26070  itg2splitlem  26075  itg2monolem1  26077  itg2gt0  26087  itg2cnlem1  26088  i1fibl  26134  itgeqa  26140  itgcn  26171  ditgex  26178  dvexp3  26304  ply1nzb  26447  ig1pval  26500  elply2  26520  dvply1  26611  aareccl  26659  dvtaylp  26703  pserdvlem2  26761  abelthlem9  26773  logtayl  26994  cxpval  26998  leibpilem2  27275  leibpi  27276  lgamgulmlem4  27365  lgamgulmlem5  27366  igamval  27380  vmaval  27446  vmaf  27452  muval  27465  prmorcht  27511  pclogsum  27548  dchrinvcl  27586  dchrptlem2  27598  bposlem5  27621  lgsval  27634  lgsfval  27635  lgsdir  27665  lgsdilem2  27666  lgsdi  27667  lgsne0  27668  gausslemma2dlem1  27699  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  padicval  27950  padicabv  27963  ostth1  27966  expsval  28817  axlowdimlem15  29540  axlowdim  29545  vtxval  29584  iedgval  29585  crctcshwlkn0lem2  30406  crctcshwlkn0lem3  30407  clwlkclwwlklem2a2  30590  psgnfzto1stlem  33708  psrmonmul  34229  xrge0iifcv  34613  xrge0iifhom  34616  ddeval1  34914  ddeval0  34915  vonf1oonfo  35969  mrsubcv  36362  mrsubrn  36365  dfrdg2  36650  finxpreclem2  38407  finxpreclem5  38412  poimirlem2  38634  poimirlem24  38656  mblfinlem2  38670  itg2addnclem  38683  itg2addnclem2  38684  itg2addnclem3  38685  itg2addnc  38686  ftc1anclem5  38709  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  fdc  38773  renegclALT  40114  cdleme50f  41693  cdlemk40  42068  cdlemk56  42122  dihval  42383  dihf11lem  42417  mapdhval  42875  hdmap1vallem  42948  readvrec  43507  evlsbagval  43708  fsuppind  43712  flcidc  44266  cantnfub  44417  cantnfresb  44420  clsk1indlem2  45136  clsk1indlem3  45137  clsk1indlem4  45138  limsup10exlem  46876  fourierdlem29  47240  fourierdlem56  47266  fourierswlem  47334  fouriersw  47335  nnfoctbdjlem  47559  isomenndlem  47634  hoidmvval  47681  hspmbl  47733  linc0scn0  49629  linc1  49631  lincext2  49661  blenval  49777  discsubclem  50271  discsubc  50272  iinfconstbas  50274  oppffn  50334  oppfvalg  50336  parhomval  50837  parswapval  50870  veronesevrowd  51148