Theorem ifex 4295

Description: Conditional operator existence. (Contributed by NM, 2-Sep-2004.)

Hypotheses

Ref	Expression
dedex.1	⊢ 𝐴 ∈ V
dedex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
ifex	⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Proof of Theorem ifex

Step	Hyp	Ref	Expression
1		dedex.1	. 2 ⊢ 𝐴 ∈ V
2		dedex.2	. 2 ⊢ 𝐵 ∈ V
3	1, 2	keepel 4294	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3351  ifcif 4225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-if 4226

This theorem is referenced by:  ifexg  4296  opex  5060  fnoe  7744  oev  7748  unxpdomlem1  8320  unxpdomlem2  8321  unxpdomlem3  8322  cantnflem1d  8749  cantnflem1  8750  iunfictbso  9137  fin23lem12  9355  axcc2lem  9460  ttukeylem3  9535  pwfseqlem2  9683  pwfseqlem3  9684  xnegex  12244  xaddval  12259  xmulval  12261  seqf1olem1  13047  expval  13069  bcval  13295  ccatlen  13557  ccatvalfn  13563  ccatalpha  13575  swrdval  13625  swrd00  13626  swrd0  13643  cshfn  13745  cshnz  13747  ofccat  13918  sgnval  14036  fsumser  14669  isumless  14784  rpnnen2lem1  15149  ruclem1  15166  sadcp1  15385  smupp1  15410  gcdval  15426  eucalgval2  15502  lcmval  15513  pcval  15756  pcmpt  15803  prmreclem2  15828  prmreclem5  15831  ramub1lem2  15938  ramcl  15940  acsfn  16527  gsumvalx  17478  mulgfval  17750  mulgval  17751  mulgfn  17752  odval  18160  odf  18163  gexval  18200  frgpup3lem  18397  dprdfeq0  18629  dmdprdsplitlem  18644  abvtrivd  19050  psrlidm  19618  psrridm  19619  mvrval2  19637  mplmonmul  19679  mplmon2  19708  coe1tmmul2fv  19863  coe1pwmulfv  19865  xrsdsval  20005  uvcvval  20342  mat1comp  20463  mat1ov  20472  matsc  20474  mat1dimid  20498  dmatmulcl  20524  scmatscmiddistr  20532  scmatscm  20537  mdetunilem9  20644  minmar1eval  20673  symgmatr01  20679  m2cpm  20766  m2cpminvid2lem  20779  decpmatid  20795  monmatcollpw  20804  mp2pm2mplem4  20834  chmatval  20854  chfacffsupp  20881  ptcmplem2  22077  ptcmplem3  22078  iccpnfhmeo  22964  xrhmeo  22965  phtpycc  23010  pcovalg  23031  pcohtpylem  23038  ovolunlem1a  23484  ovolunlem1  23485  ovolicc1  23504  ioorval  23562  mbfmax  23636  i1f1lem  23676  itg11  23678  itg1addlem3  23685  i1fres  23692  itg1climres  23701  mbfi1fseqlem4  23705  mbfi1fseqlem6  23707  mbfi1flimlem  23709  mbfi1flim  23710  itg2uba  23730  itg2splitlem  23735  itg2monolem1  23737  itg2gt0  23747  itg2cnlem1  23748  i1fibl  23794  itgeqa  23800  itgcn  23829  ditgex  23836  dvexp3  23961  ply1nzb  24102  ig1pval  24152  elply2  24172  dvply1  24259  aareccl  24301  dvtaylp  24344  pserdvlem2  24402  abelthlem9  24414  logtayl  24627  cxpval  24631  leibpilem2  24889  leibpi  24890  lgamgulmlem4  24979  lgamgulmlem5  24980  igamval  24994  vmaval  25060  vmaf  25066  muval  25079  prmorcht  25125  pclogsum  25161  dchrinvcl  25199  dchrptlem2  25211  bposlem5  25234  lgsval  25247  lgsfval  25248  lgsdir  25278  lgsdilem2  25279  lgsdi  25280  lgsne0  25281  gausslemma2dlem1  25312  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  padicval  25527  padicabv  25540  ostth1  25543  axlowdimlem15  26057  axlowdim  26062  vtxval  26099  iedgval  26100  vtxvalOLD  26101  iedgvalOLD  26102  crctcshwlkn0lem2  26939  crctcshwlkn0lem3  26940  clwlkclwwlklem2a2  27143  psgnfzto1stlem  30190  xrge0iifcv  30320  xrge0iifhom  30323  ddeval1  30637  ddeval0  30638  mrsubcv  31745  mrsubrn  31748  dfrdg2  32037  finxpreclem2  33564  finxpreclem5  33569  poimirlem2  33744  poimirlem24  33766  mblfinlem2  33780  itg2addnclem  33793  itg2addnclem2  33794  itg2addnclem3  33795  itg2addnc  33796  ftc1anclem5  33821  ftc1anclem7  33823  ftc1anclem8  33824  ftc1anc  33825  fdc  33873  renegclALT  34771  cdleme50f  36351  cdlemk40  36726  cdlemk56  36780  dihval  37042  dihf11lem  37076  mapdhval  37534  hdmap1vallem  37607  flcidc  38270  clsk1indlem2  38866  clsk1indlem3  38867  clsk1indlem4  38868  limsup10exlem  40522  fourierdlem29  40870  fourierdlem56  40896  fourierswlem  40964  fouriersw  40965  nnfoctbdjlem  41189  isomenndlem  41264  hoidmvval  41311  hspmbl  41363  linc0scn0  42740  linc1  42742  lincext2  42772  blenval  42893