Theorem ifex 4518

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  opexOLD  5412  fnoe  8438  oev  8442  unxpdomlem1  9159  unxpdomlem2  9160  unxpdomlem3  9161  cantnflem1d  9600  cantnflem1  9601  ssttrcl  9627  ttrcltr  9628  ttrclselem2  9638  iunfictbso  10027  fin23lem12  10244  axcc2lem  10349  ttukeylem3  10424  pwfseqlem2  10573  pwfseqlem3  10574  xnegex  13151  xaddval  13166  xmulval  13168  seqf1olem1  13994  expval  14016  bcval  14257  ccatlen  14528  ccatvalfn  14534  ccatalpha  14547  swrdval  14597  swrd00  14598  swrd0  14612  cshfn  14743  cshnz  14745  ofccat  14922  sgnval  15041  fsumser  15683  isumless  15801  rpnnen2lem1  16172  ruclem1  16189  sadcp1  16415  smupp1  16440  gcdval  16456  eucalgval2  16541  lcmval  16552  pcval  16806  pcmpt  16854  prmreclem2  16879  prmreclem5  16882  ramub1lem2  16989  ramcl  16991  acsfn  17616  gsumvalx  18635  mulgfval  19036  mulgfvalALT  19037  mulgval  19038  mulgfn  19039  odval  19500  odf  19503  gexval  19544  frgpup3lem  19743  dprdfeq0  19990  dmdprdsplitlem  20005  abvtrivd  20800  xrsdsval  21400  uvcvval  21776  psrlidm  21950  psrridm  21951  psrascl  21967  mvrval2  21971  mplmonmul  22024  mplmon2  22049  psdmplcl  22138  coe1tmmul2fv  22253  coe1pwmulfv  22255  mat1comp  22415  mat1ov  22423  matsc  22425  mat1dimid  22449  dmatmulcl  22475  scmatscmiddistr  22483  scmatscm  22488  mdetunilem9  22595  minmar1eval  22624  symgmatr01  22629  m2cpm  22716  m2cpminvid2lem  22729  decpmatid  22745  monmatcollpw  22754  mp2pm2mplem4  22784  chmatval  22804  chfacffsupp  22831  ptcmplem2  24028  ptcmplem3  24029  iccpnfhmeo  24922  xrhmeo  24923  phtpycc  24968  pcovalg  24989  pcohtpylem  24996  ovolunlem1a  25473  ovolunlem1  25474  ovolicc1  25493  ioorval  25551  mbfmax  25626  i1f1lem  25666  itg11  25668  itg1addlem3  25675  i1fres  25682  itg1climres  25691  mbfi1fseqlem4  25695  mbfi1fseqlem6  25697  mbfi1flimlem  25699  mbfi1flim  25700  itg2uba  25720  itg2splitlem  25725  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  i1fibl  25785  itgeqa  25791  itgcn  25822  ditgex  25829  dvexp3  25955  ply1nzb  26098  ig1pval  26151  elply2  26171  dvply1  26260  aareccl  26303  dvtaylp  26347  pserdvlem2  26406  abelthlem9  26418  logtayl  26637  cxpval  26641  leibpilem2  26918  leibpi  26919  lgamgulmlem4  27009  lgamgulmlem5  27010  igamval  27024  vmaval  27090  vmaf  27096  muval  27109  prmorcht  27155  pclogsum  27192  dchrinvcl  27230  dchrptlem2  27242  bposlem5  27265  lgsval  27278  lgsfval  27279  lgsdir  27309  lgsdilem2  27310  lgsdi  27311  lgsne0  27312  gausslemma2dlem1  27343  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  padicval  27594  padicabv  27607  ostth1  27610  expsval  28431  axlowdimlem15  29039  axlowdim  29044  vtxval  29083  iedgval  29084  crctcshwlkn0lem2  29894  crctcshwlkn0lem3  29895  clwlkclwwlklem2a2  30078  psgnfzto1stlem  33176  psrmonmul  33709  xrge0iifcv  34094  xrge0iifhom  34097  ddeval1  34394  ddeval0  34395  mrsubcv  35708  mrsubrn  35711  dfrdg2  35991  finxpreclem2  37720  finxpreclem5  37725  poimirlem2  37957  poimirlem24  37979  mblfinlem2  37993  itg2addnclem  38006  itg2addnclem2  38007  itg2addnclem3  38008  itg2addnc  38009  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  fdc  38080  renegclALT  39423  cdleme50f  41002  cdlemk40  41377  cdlemk56  41431  dihval  41692  dihf11lem  41726  mapdhval  42184  hdmap1vallem  42257  readvrec  42808  evlsbagval  43016  fsuppind  43037  flcidc  43616  cantnfub  43767  cantnfresb  43770  clsk1indlem2  44487  clsk1indlem3  44488  clsk1indlem4  44489  limsup10exlem  46218  fourierdlem29  46582  fourierdlem56  46608  fourierswlem  46676  fouriersw  46677  nnfoctbdjlem  46901  isomenndlem  46976  hoidmvval  47023  hspmbl  47075  linc0scn0  48911  linc1  48913  lincext2  48943  blenval  49059  discsubclem  49550  discsubc  49551  iinfconstbas  49553  oppffn  49611  oppfvalg  49613