Theorem ifex 4536

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ifcif 4485

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  opexOLD  5438  fnoe  8554  oev  8558  unxpdomlem1  9283  unxpdomlem2  9284  unxpdomlem3  9285  cantnflem1d  9724  cantnflem1  9725  ssttrcl  9751  ttrcltr  9752  ttrclselem2  9762  iunfictbso  10230  fin23lem12  10446  axcc2lem  10551  ttukeylem3  10626  pwfseqlem2  10781  pwfseqlem3  10782  xnegex  13376  xaddval  13391  xmulval  13393  seqf1olem1  14222  expval  14244  bcval  14487  ccatlen  14759  ccatvalfn  14765  ccatalpha  14779  swrdval  14831  swrd00  14832  swrd0  14848  cshfn  14981  cshnz  14983  ofccat  15163  sgnval  15282  sgndm  15290  fsumser  15937  isumless  16055  rpnnen2lem1  16423  ruclem1  16440  sadcp1  16666  smupp1  16691  gcdval  16707  eucalgval2  16797  lcmval  16808  pcval  17063  pcmpt  17111  prmreclem2  17136  prmreclem5  17139  ramub1lem2  17246  ramcl  17248  acsfn  17874  gsumvalx  18906  mulgfval  19320  mulgfvalALT  19321  mulgval  19322  mulgfn  19323  odval  19790  odf  19793  gexval  19834  frgpup3lem  20033  dprdfeq0  20280  dmdprdsplitlem  20295  abvtrivd  21131  xrsdsval  21759  uvcvval  22136  psrlidm  22313  psrridm  22314  psrascl  22330  mvrval2  22334  mplmonmul  22389  mplmon2  22414  psdmplcl  22527  coe1tmmul2fv  22641  coe1pwmulfv  22643  mat1comp  22799  mat1ov  22807  matsc  22809  mat1dimid  22833  dmatmulcl  22859  scmatscmiddistr  22867  scmatscm  22872  mdetunilem9  22979  minmar1eval  23008  symgmatr01  23013  m2cpm  23103  m2cpminvid2lem  23116  decpmatid  23132  monmatcollpw  23141  mp2pm2mplem4  23171  chmatval  23191  chfacffsupp  23218  ptcmplem2  24416  ptcmplem3  24417  iccpnfhmeo  25310  xrhmeo  25311  phtpycc  25356  pcovalg  25377  pcohtpylem  25384  ovolunlem1a  25861  ovolunlem1  25862  ovolicc1  25881  ioorval  25939  mbfmax  26014  i1f1lem  26054  itg11  26056  itg1addlem3  26063  i1fres  26070  itg1climres  26079  mbfi1fseqlem4  26083  mbfi1fseqlem6  26085  mbfi1flimlem  26087  mbfi1flim  26088  itg2uba  26108  itg2splitlem  26113  itg2monolem1  26115  itg2gt0  26125  itg2cnlem1  26126  i1fibl  26172  itgeqa  26178  itgcn  26209  ditgex  26216  dvexp3  26342  ply1nzb  26485  ig1pval  26538  elply2  26558  dvply1  26649  aareccl  26699  dvtaylp  26743  pserdvlem2  26801  abelthlem9  26813  logtayl  27034  cxpval  27038  leibpilem2  27315  leibpi  27316  lgamgulmlem4  27405  lgamgulmlem5  27406  igamval  27420  vmaval  27486  vmaf  27492  muval  27505  prmorcht  27551  pclogsum  27588  dchrinvcl  27626  dchrptlem2  27638  bposlem5  27661  lgsval  27674  lgsfval  27675  lgsdir  27705  lgsdilem2  27706  lgsdi  27707  lgsne0  27708  gausslemma2dlem1  27739  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  padicval  27990  padicabv  28003  ostth1  28006  expsval  28857  axlowdimlem15  29580  axlowdim  29585  vtxval  29624  iedgval  29625  crctcshwlkn0lem2  30446  crctcshwlkn0lem3  30447  clwlkclwwlklem2a2  30630  psgnfzto1stlem  33750  psrmonmul  34286  xrge0iifcv  34670  xrge0iifhom  34673  ddeval1  34971  ddeval0  34972  vonf1oonfo  36083  mrsubcv  36476  mrsubrn  36479  dfrdg2  36765  finxpreclem2  38574  finxpreclem5  38579  poimirlem2  38801  poimirlem24  38823  mblfinlem2  38837  itg2addnclem  38850  itg2addnclem2  38851  itg2addnclem3  38852  itg2addnc  38853  ftc1anclem5  38876  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  fdc  38938  renegclALT  40279  cdleme50f  41858  cdlemk40  42233  cdlemk56  42287  dihval  42548  dihf11lem  42582  mapdhval  43040  hdmap1vallem  43113  readvrec  43673  evlsbagval  43874  fsuppind  43878  flcidc  44427  cantnfub  44578  cantnfresb  44581  clsk1indlem2  45297  clsk1indlem3  45298  clsk1indlem4  45299  limsup10exlem  47049  fourierdlem29  47413  fourierdlem56  47439  fourierswlem  47507  fouriersw  47508  nnfoctbdjlem  47732  isomenndlem  47807  hoidmvval  47854  hspmbl  47906  linc0scn0  49860  linc1  49862  lincext2  49892  blenval  50008  discsubclem  50502  discsubc  50503  iinfconstbas  50505  oppffn  50565  oppfvalg  50567  parhomval  51068  parswapval  51101  veronesevrowd  51401