Theorem ifex 4521

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4471

This theorem is referenced by:  opex  5399  fnoe  8420  oev  8424  unxpdomlem1  9135  unxpdomlem2  9136  unxpdomlem3  9137  cantnflem1d  9573  cantnflem1  9574  ssttrcl  9600  ttrcltr  9601  ttrclselem2  9611  iunfictbso  10000  fin23lem12  10217  axcc2lem  10322  ttukeylem3  10397  pwfseqlem2  10545  pwfseqlem3  10546  xnegex  13102  xaddval  13117  xmulval  13119  seqf1olem1  13943  expval  13965  bcval  14206  ccatlen  14477  ccatvalfn  14483  ccatalpha  14496  swrdval  14546  swrd00  14547  swrd0  14561  cshfn  14692  cshnz  14694  ofccat  14871  sgnval  14990  fsumser  15632  isumless  15747  rpnnen2lem1  16118  ruclem1  16135  sadcp1  16361  smupp1  16386  gcdval  16402  eucalgval2  16487  lcmval  16498  pcval  16751  pcmpt  16799  prmreclem2  16824  prmreclem5  16827  ramub1lem2  16934  ramcl  16936  acsfn  17560  gsumvalx  18579  mulgfval  18977  mulgfvalALT  18978  mulgval  18979  mulgfn  18980  odval  19441  odf  19444  gexval  19485  frgpup3lem  19684  dprdfeq0  19931  dmdprdsplitlem  19946  abvtrivd  20742  xrsdsval  21342  uvcvval  21718  psrlidm  21894  psrridm  21895  psrascl  21911  mvrval2  21915  mplmonmul  21966  mplmon2  21991  psdmplcl  22072  coe1tmmul2fv  22187  coe1pwmulfv  22189  mat1comp  22350  mat1ov  22358  matsc  22360  mat1dimid  22384  dmatmulcl  22410  scmatscmiddistr  22418  scmatscm  22423  mdetunilem9  22530  minmar1eval  22559  symgmatr01  22564  m2cpm  22651  m2cpminvid2lem  22664  decpmatid  22680  monmatcollpw  22689  mp2pm2mplem4  22719  chmatval  22739  chfacffsupp  22766  ptcmplem2  23963  ptcmplem3  23964  iccpnfhmeo  24865  xrhmeo  24866  phtpycc  24912  pcovalg  24934  pcohtpylem  24941  ovolunlem1a  25419  ovolunlem1  25420  ovolicc1  25439  ioorval  25497  mbfmax  25572  i1f1lem  25612  itg11  25614  itg1addlem3  25621  i1fres  25628  itg1climres  25637  mbfi1fseqlem4  25641  mbfi1fseqlem6  25643  mbfi1flimlem  25645  mbfi1flim  25646  itg2uba  25666  itg2splitlem  25671  itg2monolem1  25673  itg2gt0  25683  itg2cnlem1  25684  i1fibl  25731  itgeqa  25737  itgcn  25768  ditgex  25775  dvexp3  25904  ply1nzb  26050  ig1pval  26103  elply2  26123  dvply1  26213  aareccl  26256  dvtaylp  26300  pserdvlem2  26360  abelthlem9  26372  logtayl  26591  cxpval  26595  leibpilem2  26873  leibpi  26874  lgamgulmlem4  26964  lgamgulmlem5  26965  igamval  26979  vmaval  27045  vmaf  27051  muval  27064  prmorcht  27110  pclogsum  27148  dchrinvcl  27186  dchrptlem2  27198  bposlem5  27221  lgsval  27234  lgsfval  27235  lgsdir  27265  lgsdilem2  27266  lgsdi  27267  lgsne0  27268  gausslemma2dlem1  27299  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  padicval  27550  padicabv  27563  ostth1  27566  expsval  28343  axlowdimlem15  28929  axlowdim  28934  vtxval  28973  iedgval  28974  crctcshwlkn0lem2  29784  crctcshwlkn0lem3  29785  clwlkclwwlklem2a2  29965  psgnfzto1stlem  33061  xrge0iifcv  33939  xrge0iifhom  33942  ddeval1  34239  ddeval0  34240  mrsubcv  35546  mrsubrn  35549  dfrdg2  35829  finxpreclem2  37424  finxpreclem5  37429  poimirlem2  37662  poimirlem24  37684  mblfinlem2  37698  itg2addnclem  37711  itg2addnclem2  37712  itg2addnclem3  37713  itg2addnc  37714  ftc1anclem5  37737  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  fdc  37785  renegclALT  39002  cdleme50f  40581  cdlemk40  40956  cdlemk56  41010  dihval  41271  dihf11lem  41305  mapdhval  41763  hdmap1vallem  41836  readvrec  42395  evlsbagval  42599  fsuppind  42623  flcidc  43203  cantnfub  43354  cantnfresb  43357  clsk1indlem2  44075  clsk1indlem3  44076  clsk1indlem4  44077  limsup10exlem  45810  fourierdlem29  46174  fourierdlem56  46200  fourierswlem  46268  fouriersw  46269  nnfoctbdjlem  46493  isomenndlem  46568  hoidmvval  46615  hspmbl  46667  linc0scn0  48455  linc1  48457  lincext2  48487  blenval  48603  discsubclem  49095  discsubc  49096  iinfconstbas  49098  oppffn  49156  oppfvalg  49158