Theorem ifex 4539

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ifcif 4488

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 4489

This theorem is referenced by:  opex  5424  fnoe  8474  oev  8478  unxpdomlem1  9197  unxpdomlem2  9198  unxpdomlem3  9199  cantnflem1d  9641  cantnflem1  9642  ssttrcl  9668  ttrcltr  9669  ttrclselem2  9679  iunfictbso  10067  fin23lem12  10284  axcc2lem  10389  ttukeylem3  10464  pwfseqlem2  10612  pwfseqlem3  10613  xnegex  13168  xaddval  13183  xmulval  13185  seqf1olem1  14006  expval  14028  bcval  14269  ccatlen  14540  ccatvalfn  14546  ccatalpha  14558  swrdval  14608  swrd00  14609  swrd0  14623  cshfn  14755  cshnz  14757  ofccat  14935  sgnval  15054  fsumser  15696  isumless  15811  rpnnen2lem1  16182  ruclem1  16199  sadcp1  16425  smupp1  16450  gcdval  16466  eucalgval2  16551  lcmval  16562  pcval  16815  pcmpt  16863  prmreclem2  16888  prmreclem5  16891  ramub1lem2  16998  ramcl  17000  acsfn  17620  gsumvalx  18603  mulgfval  19001  mulgfvalALT  19002  mulgval  19003  mulgfn  19004  odval  19464  odf  19467  gexval  19508  frgpup3lem  19707  dprdfeq0  19954  dmdprdsplitlem  19969  abvtrivd  20741  xrsdsval  21327  uvcvval  21695  psrlidm  21871  psrridm  21872  psrascl  21888  mvrval2  21892  mplmonmul  21943  mplmon2  21968  psdmplcl  22049  coe1tmmul2fv  22164  coe1pwmulfv  22166  mat1comp  22327  mat1ov  22335  matsc  22337  mat1dimid  22361  dmatmulcl  22387  scmatscmiddistr  22395  scmatscm  22400  mdetunilem9  22507  minmar1eval  22536  symgmatr01  22541  m2cpm  22628  m2cpminvid2lem  22641  decpmatid  22657  monmatcollpw  22666  mp2pm2mplem4  22696  chmatval  22716  chfacffsupp  22743  ptcmplem2  23940  ptcmplem3  23941  iccpnfhmeo  24843  xrhmeo  24844  phtpycc  24890  pcovalg  24912  pcohtpylem  24919  ovolunlem1a  25397  ovolunlem1  25398  ovolicc1  25417  ioorval  25475  mbfmax  25550  i1f1lem  25590  itg11  25592  itg1addlem3  25599  i1fres  25606  itg1climres  25615  mbfi1fseqlem4  25619  mbfi1fseqlem6  25621  mbfi1flimlem  25623  mbfi1flim  25624  itg2uba  25644  itg2splitlem  25649  itg2monolem1  25651  itg2gt0  25661  itg2cnlem1  25662  i1fibl  25709  itgeqa  25715  itgcn  25746  ditgex  25753  dvexp3  25882  ply1nzb  26028  ig1pval  26081  elply2  26101  dvply1  26191  aareccl  26234  dvtaylp  26278  pserdvlem2  26338  abelthlem9  26350  logtayl  26569  cxpval  26573  leibpilem2  26851  leibpi  26852  lgamgulmlem4  26942  lgamgulmlem5  26943  igamval  26957  vmaval  27023  vmaf  27029  muval  27042  prmorcht  27088  pclogsum  27126  dchrinvcl  27164  dchrptlem2  27176  bposlem5  27199  lgsval  27212  lgsfval  27213  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  gausslemma2dlem1  27277  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  padicval  27528  padicabv  27541  ostth1  27544  expsval  28311  axlowdimlem15  28883  axlowdim  28888  vtxval  28927  iedgval  28928  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  clwlkclwwlklem2a2  29922  psgnfzto1stlem  33057  xrge0iifcv  33924  xrge0iifhom  33927  ddeval1  34224  ddeval0  34225  mrsubcv  35497  mrsubrn  35500  dfrdg2  35783  finxpreclem2  37378  finxpreclem5  37383  poimirlem2  37616  poimirlem24  37638  mblfinlem2  37652  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  itg2addnc  37668  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  fdc  37739  renegclALT  38956  cdleme50f  40536  cdlemk40  40911  cdlemk56  40965  dihval  41226  dihf11lem  41260  mapdhval  41718  hdmap1vallem  41791  readvrec  42350  evlsbagval  42554  fsuppind  42578  flcidc  43159  cantnfub  43310  cantnfresb  43313  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  limsup10exlem  45770  fourierdlem29  46134  fourierdlem56  46160  fourierswlem  46228  fouriersw  46229  nnfoctbdjlem  46453  isomenndlem  46528  hoidmvval  46575  hspmbl  46627  linc0scn0  48412  linc1  48414  lincext2  48444  blenval  48560  discsubclem  49052  discsubc  49053  iinfconstbas  49055  oppffn  49113  oppfvalg  49115