Theorem ifex 4540

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ifcif 4489

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  opexOLD  5448  fnoe  8497  oev  8501  unxpdomlem1  9219  unxpdomlem2  9220  unxpdomlem3  9221  cantnflem1d  9660  cantnflem1  9661  ssttrcl  9687  ttrcltr  9688  ttrclselem2  9698  iunfictbso  10110  fin23lem12  10326  axcc2lem  10431  ttukeylem3  10506  pwfseqlem2  10655  pwfseqlem3  10656  xnegex  13245  xaddval  13260  xmulval  13262  seqf1olem1  14090  expval  14112  bcval  14353  ccatlen  14625  ccatvalfn  14631  ccatalpha  14645  swrdval  14696  swrd00  14697  swrd0  14713  cshfn  14846  cshnz  14848  ofccat  15025  sgnval  15144  sgndm  15152  fsumser  15799  isumless  15917  rpnnen2lem1  16287  ruclem1  16304  sadcp1  16530  smupp1  16555  gcdval  16571  eucalgval2  16656  lcmval  16667  pcval  16921  pcmpt  16969  prmreclem2  16994  prmreclem5  16997  ramub1lem2  17104  ramcl  17106  acsfn  17732  gsumvalx  18755  mulgfval  19158  mulgfvalALT  19159  mulgval  19160  mulgfn  19161  odval  19627  odf  19630  gexval  19671  frgpup3lem  19870  dprdfeq0  20117  dmdprdsplitlem  20132  abvtrivd  20964  xrsdsval  21590  uvcvval  21965  psrlidm  22140  psrridm  22141  psrascl  22157  mvrval2  22161  mplmonmul  22216  mplmon2  22241  psdmplcl  22354  coe1tmmul2fv  22468  coe1pwmulfv  22470  mat1comp  22626  mat1ov  22634  matsc  22636  mat1dimid  22660  dmatmulcl  22686  scmatscmiddistr  22694  scmatscm  22699  mdetunilem9  22806  minmar1eval  22835  symgmatr01  22840  m2cpm  22927  m2cpminvid2lem  22940  decpmatid  22956  monmatcollpw  22965  mp2pm2mplem4  22995  chmatval  23015  chfacffsupp  23042  ptcmplem2  24239  ptcmplem3  24240  iccpnfhmeo  25133  xrhmeo  25134  phtpycc  25179  pcovalg  25200  pcohtpylem  25207  ovolunlem1a  25684  ovolunlem1  25685  ovolicc1  25704  ioorval  25762  mbfmax  25837  i1f1lem  25877  itg11  25879  itg1addlem3  25886  i1fres  25893  itg1climres  25902  mbfi1fseqlem4  25906  mbfi1fseqlem6  25908  mbfi1flimlem  25910  mbfi1flim  25911  itg2uba  25931  itg2splitlem  25936  itg2monolem1  25938  itg2gt0  25948  itg2cnlem1  25949  i1fibl  25996  itgeqa  26002  itgcn  26033  ditgex  26040  dvexp3  26166  ply1nzb  26309  ig1pval  26362  elply2  26382  dvply1  26474  aareccl  26518  dvtaylp  26562  pserdvlem2  26620  abelthlem9  26632  logtayl  26854  cxpval  26858  leibpilem2  27135  leibpi  27136  lgamgulmlem4  27225  lgamgulmlem5  27226  igamval  27240  vmaval  27306  vmaf  27312  muval  27325  prmorcht  27371  pclogsum  27408  dchrinvcl  27446  dchrptlem2  27458  bposlem5  27481  lgsval  27494  lgsfval  27495  lgsdir  27525  lgsdilem2  27526  lgsdi  27527  lgsne0  27528  gausslemma2dlem1  27559  pntrlog2bndlem4  27773  pntrlog2bndlem5  27774  padicval  27810  padicabv  27823  ostth1  27826  expsval  28647  axlowdimlem15  29335  axlowdim  29340  vtxval  29379  iedgval  29380  crctcshwlkn0lem2  30189  crctcshwlkn0lem3  30190  clwlkclwwlklem2a2  30373  psgnfzto1stlem  33443  psrmonmul  33963  xrge0iifcv  34347  xrge0iifhom  34350  ddeval1  34648  ddeval0  34649  vonf1oonfo  35615  mrsubcv  36015  mrsubrn  36018  dfrdg2  36298  finxpreclem2  38069  finxpreclem5  38074  poimirlem2  38306  poimirlem24  38328  mblfinlem2  38342  itg2addnclem  38355  itg2addnclem2  38356  itg2addnclem3  38357  itg2addnc  38358  ftc1anclem5  38381  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  fdc  38429  renegclALT  39770  cdleme50f  41349  cdlemk40  41724  cdlemk56  41778  dihval  42039  dihf11lem  42073  mapdhval  42531  hdmap1vallem  42604  readvrec  43156  evlsbagval  43351  fsuppind  43355  flcidc  43930  cantnfub  44081  cantnfresb  44084  clsk1indlem2  44801  clsk1indlem3  44802  clsk1indlem4  44803  limsup10exlem  46519  fourierdlem29  46883  fourierdlem56  46909  fourierswlem  46977  fouriersw  46978  nnfoctbdjlem  47202  isomenndlem  47277  hoidmvval  47324  hspmbl  47376  linc0scn0  49236  linc1  49238  lincext2  49268  blenval  49384  discsubclem  49874  discsubc  49875  iinfconstbas  49877  oppffn  49935  oppfvalg  49937