Theorem ifex 4533

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  opexOLD  5433  fnoe  8511  oev  8515  unxpdomlem1  9240  unxpdomlem2  9241  unxpdomlem3  9242  cantnflem1d  9682  cantnflem1  9683  ssttrcl  9709  ttrcltr  9710  ttrclselem2  9720  iunfictbso  10186  fin23lem12  10402  axcc2lem  10507  ttukeylem3  10582  pwfseqlem2  10737  pwfseqlem3  10738  xnegex  13331  xaddval  13346  xmulval  13348  seqf1olem1  14177  expval  14199  bcval  14441  ccatlen  14713  ccatvalfn  14719  ccatalpha  14733  swrdval  14784  swrd00  14785  swrd0  14801  cshfn  14934  cshnz  14936  ofccat  15115  sgnval  15234  sgndm  15242  fsumser  15889  isumless  16007  rpnnen2lem1  16375  ruclem1  16392  sadcp1  16618  smupp1  16643  gcdval  16659  eucalgval2  16749  lcmval  16760  pcval  17015  pcmpt  17063  prmreclem2  17088  prmreclem5  17091  ramub1lem2  17198  ramcl  17200  acsfn  17826  gsumvalx  18858  mulgfval  19272  mulgfvalALT  19273  mulgval  19274  mulgfn  19275  odval  19741  odf  19744  gexval  19785  frgpup3lem  19984  dprdfeq0  20231  dmdprdsplitlem  20246  abvtrivd  21082  xrsdsval  21710  uvcvval  22085  psrlidm  22262  psrridm  22263  psrascl  22279  mvrval2  22283  mplmonmul  22338  mplmon2  22363  psdmplcl  22476  coe1tmmul2fv  22590  coe1pwmulfv  22592  mat1comp  22748  mat1ov  22756  matsc  22758  mat1dimid  22782  dmatmulcl  22808  scmatscmiddistr  22816  scmatscm  22821  mdetunilem9  22928  minmar1eval  22957  symgmatr01  22962  m2cpm  23052  m2cpminvid2lem  23065  decpmatid  23081  monmatcollpw  23090  mp2pm2mplem4  23120  chmatval  23140  chfacffsupp  23167  ptcmplem2  24365  ptcmplem3  24366  iccpnfhmeo  25259  xrhmeo  25260  phtpycc  25305  pcovalg  25326  pcohtpylem  25333  ovolunlem1a  25810  ovolunlem1  25811  ovolicc1  25830  ioorval  25888  mbfmax  25963  i1f1lem  26003  itg11  26005  itg1addlem3  26012  i1fres  26019  itg1climres  26028  mbfi1fseqlem4  26032  mbfi1fseqlem6  26034  mbfi1flimlem  26036  mbfi1flim  26037  itg2uba  26057  itg2splitlem  26062  itg2monolem1  26064  itg2gt0  26074  itg2cnlem1  26075  i1fibl  26121  itgeqa  26127  itgcn  26158  ditgex  26165  dvexp3  26291  ply1nzb  26434  ig1pval  26487  elply2  26507  dvply1  26598  aareccl  26646  dvtaylp  26690  pserdvlem2  26748  abelthlem9  26760  logtayl  26981  cxpval  26985  leibpilem2  27262  leibpi  27263  lgamgulmlem4  27352  lgamgulmlem5  27353  igamval  27367  vmaval  27433  vmaf  27439  muval  27452  prmorcht  27498  pclogsum  27535  dchrinvcl  27573  dchrptlem2  27585  bposlem5  27608  lgsval  27621  lgsfval  27622  lgsdir  27652  lgsdilem2  27653  lgsdi  27654  lgsne0  27655  gausslemma2dlem1  27686  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  padicval  27937  padicabv  27950  ostth1  27953  expsval  28804  axlowdimlem15  29527  axlowdim  29532  vtxval  29571  iedgval  29572  crctcshwlkn0lem2  30393  crctcshwlkn0lem3  30394  clwlkclwwlklem2a2  30577  psgnfzto1stlem  33654  psrmonmul  34175  xrge0iifcv  34559  xrge0iifhom  34562  ddeval1  34860  ddeval0  34861  vonf1oonfo  35877  mrsubcv  36254  mrsubrn  36257  dfrdg2  36537  finxpreclem2  38293  finxpreclem5  38298  poimirlem2  38520  poimirlem24  38542  mblfinlem2  38556  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  itg2addnc  38572  ftc1anclem5  38595  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  fdc  38659  renegclALT  40000  cdleme50f  41579  cdlemk40  41954  cdlemk56  42008  dihval  42269  dihf11lem  42303  mapdhval  42761  hdmap1vallem  42834  readvrec  43393  evlsbagval  43594  fsuppind  43598  flcidc  44156  cantnfub  44307  cantnfresb  44310  clsk1indlem2  45027  clsk1indlem3  45028  clsk1indlem4  45029  limsup10exlem  46751  fourierdlem29  47115  fourierdlem56  47141  fourierswlem  47209  fouriersw  47210  nnfoctbdjlem  47434  isomenndlem  47509  hoidmvval  47556  hspmbl  47608  linc0scn0  49504  linc1  49506  lincext2  49536  blenval  49652  discsubclem  50140  discsubc  50141  iinfconstbas  50143  oppffn  50201  oppfvalg  50203  veronesevrowd  50948