Theorem ifex 4489

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

Syntax hints:   ∈ wcel 2110  Vcvv 3408  ifcif 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4440

This theorem is referenced by:  opex  5348  fnoe  8237  oev  8241  unxpdomlem1  8882  unxpdomlem2  8883  unxpdomlem3  8884  cantnflem1d  9303  cantnflem1  9304  iunfictbso  9728  fin23lem12  9945  axcc2lem  10050  ttukeylem3  10125  pwfseqlem2  10273  pwfseqlem3  10274  xnegex  12798  xaddval  12813  xmulval  12815  seqf1olem1  13615  expval  13637  bcval  13870  ccatlen  14130  ccatlenOLD  14131  ccatvalfn  14138  ccatalpha  14150  swrdval  14208  swrd00  14209  swrd0  14223  cshfn  14355  cshnz  14357  ofccat  14532  sgnval  14651  fsumser  15294  isumless  15409  rpnnen2lem1  15775  ruclem1  15792  sadcp1  16014  smupp1  16039  gcdval  16055  eucalgval2  16138  lcmval  16149  pcval  16397  pcmpt  16445  prmreclem2  16470  prmreclem5  16473  ramub1lem2  16580  ramcl  16582  acsfn  17162  gsumvalx  18148  mulgfval  18490  mulgfvalALT  18491  mulgval  18492  mulgfn  18493  odval  18926  odf  18929  gexval  18967  frgpup3lem  19167  dprdfeq0  19409  dmdprdsplitlem  19424  abvtrivd  19876  xrsdsval  20407  uvcvval  20748  psrlidm  20928  psrridm  20929  mvrval2  20947  mplmonmul  20993  mplmon2  21019  coe1tmmul2fv  21199  coe1pwmulfv  21201  mat1comp  21337  mat1ov  21345  matsc  21347  mat1dimid  21371  dmatmulcl  21397  scmatscmiddistr  21405  scmatscm  21410  mdetunilem9  21517  minmar1eval  21546  symgmatr01  21551  m2cpm  21638  m2cpminvid2lem  21651  decpmatid  21667  monmatcollpw  21676  mp2pm2mplem4  21706  chmatval  21726  chfacffsupp  21753  ptcmplem2  22950  ptcmplem3  22951  iccpnfhmeo  23842  xrhmeo  23843  phtpycc  23888  pcovalg  23909  pcohtpylem  23916  ovolunlem1a  24393  ovolunlem1  24394  ovolicc1  24413  ioorval  24471  mbfmax  24546  i1f1lem  24586  itg11  24588  itg1addlem3  24595  i1fres  24603  itg1climres  24612  mbfi1fseqlem4  24616  mbfi1fseqlem6  24618  mbfi1flimlem  24620  mbfi1flim  24621  itg2uba  24641  itg2splitlem  24646  itg2monolem1  24648  itg2gt0  24658  itg2cnlem1  24659  i1fibl  24705  itgeqa  24711  itgcn  24742  ditgex  24749  dvexp3  24875  ply1nzb  25020  ig1pval  25070  elply2  25090  dvply1  25177  aareccl  25219  dvtaylp  25262  pserdvlem2  25320  abelthlem9  25332  logtayl  25548  cxpval  25552  leibpilem2  25824  leibpi  25825  lgamgulmlem4  25914  lgamgulmlem5  25915  igamval  25929  vmaval  25995  vmaf  26001  muval  26014  prmorcht  26060  pclogsum  26096  dchrinvcl  26134  dchrptlem2  26146  bposlem5  26169  lgsval  26182  lgsfval  26183  lgsdir  26213  lgsdilem2  26214  lgsdi  26215  lgsne0  26216  gausslemma2dlem1  26247  pntrlog2bndlem4  26461  pntrlog2bndlem5  26462  padicval  26498  padicabv  26511  ostth1  26514  axlowdimlem15  27047  axlowdim  27052  vtxval  27091  iedgval  27092  crctcshwlkn0lem2  27895  crctcshwlkn0lem3  27896  clwlkclwwlklem2a2  28076  psgnfzto1stlem  31086  xrge0iifcv  31598  xrge0iifhom  31601  ddeval1  31914  ddeval0  31915  mrsubcv  33185  mrsubrn  33188  dfrdg2  33490  ssttrcl  33514  ttrcltr  33515  finxpreclem2  35298  finxpreclem5  35303  poimirlem2  35516  poimirlem24  35538  mblfinlem2  35552  itg2addnclem  35565  itg2addnclem2  35566  itg2addnclem3  35567  itg2addnc  35568  ftc1anclem5  35591  ftc1anclem7  35593  ftc1anclem8  35594  ftc1anc  35595  fdc  35640  renegclALT  36714  cdleme50f  38293  cdlemk40  38668  cdlemk56  38722  dihval  38983  dihf11lem  39017  mapdhval  39475  hdmap1vallem  39548  evlsbagval  39985  fsuppind  39989  mhphf  39995  flcidc  40702  clsk1indlem2  41329  clsk1indlem3  41330  clsk1indlem4  41331  limsup10exlem  42988  fourierdlem29  43352  fourierdlem56  43378  fourierswlem  43446  fouriersw  43447  nnfoctbdjlem  43668  isomenndlem  43743  hoidmvval  43790  hspmbl  43842  linc0scn0  45437  linc1  45439  lincext2  45469  blenval  45590