Theorem ifex 4505

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4455

This theorem is referenced by:  opexOLD  5404  fnoe  8435  oev  8439  unxpdomlem1  9156  unxpdomlem2  9157  unxpdomlem3  9158  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  20804  xrsdsval  21386  uvcvval  21761  psrlidm  21936  psrridm  21937  psrascl  21953  mvrval2  21957  mplmonmul  22012  mplmon2  22037  psdmplcl  22150  coe1tmmul2fv  22264  coe1pwmulfv  22266  mat1comp  22423  mat1ov  22431  matsc  22433  mat1dimid  22457  dmatmulcl  22483  scmatscmiddistr  22491  scmatscm  22496  mdetunilem9  22603  minmar1eval  22632  symgmatr01  22637  m2cpm  22724  m2cpminvid2lem  22737  decpmatid  22753  monmatcollpw  22762  mp2pm2mplem4  22792  chmatval  22812  chfacffsupp  22839  ptcmplem2  24036  ptcmplem3  24037  iccpnfhmeo  24930  xrhmeo  24931  phtpycc  24976  pcovalg  24997  pcohtpylem  25004  ovolunlem1a  25481  ovolunlem1  25482  ovolicc1  25501  ioorval  25559  mbfmax  25634  i1f1lem  25674  itg11  25676  itg1addlem3  25683  i1fres  25690  itg1climres  25699  mbfi1fseqlem4  25703  mbfi1fseqlem6  25705  mbfi1flimlem  25707  mbfi1flim  25708  itg2uba  25728  itg2splitlem  25733  itg2monolem1  25735  itg2gt0  25745  itg2cnlem1  25746  i1fibl  25793  itgeqa  25799  itgcn  25830  ditgex  25837  dvexp3  25963  ply1nzb  26106  ig1pval  26159  elply2  26179  dvply1  26268  aareccl  26310  dvtaylp  26353  pserdvlem2  26411  abelthlem9  26423  logtayl  26642  cxpval  26646  leibpilem2  26923  leibpi  26924  lgamgulmlem4  27013  lgamgulmlem5  27014  igamval  27028  vmaval  27094  vmaf  27100  muval  27113  prmorcht  27159  pclogsum  27196  dchrinvcl  27234  dchrptlem2  27246  bposlem5  27269  lgsval  27282  lgsfval  27283  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  gausslemma2dlem1  27347  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  padicval  27598  padicabv  27611  ostth1  27614  expsval  28435  axlowdimlem15  29043  axlowdim  29048  vtxval  29087  iedgval  29088  crctcshwlkn0lem2  29897  crctcshwlkn0lem3  29898  clwlkclwwlklem2a2  30081  psgnfzto1stlem  33181  psrmonmul  33734  xrge0iifcv  34118  xrge0iifhom  34121  ddeval1  34418  ddeval0  34419  mrsubcv  35738  mrsubrn  35741  dfrdg2  36021  finxpreclem2  37752  finxpreclem5  37757  poimirlem2  37989  poimirlem24  38011  mblfinlem2  38025  itg2addnclem  38038  itg2addnclem2  38039  itg2addnclem3  38040  itg2addnc  38041  ftc1anclem5  38064  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  fdc  38112  renegclALT  39455  cdleme50f  41034  cdlemk40  41409  cdlemk56  41463  dihval  41724  dihf11lem  41758  mapdhval  42216  hdmap1vallem  42289  readvrec  42839  evlsbagval  43036  fsuppind  43040  flcidc  43615  cantnfub  43766  cantnfresb  43769  clsk1indlem2  44486  clsk1indlem3  44487  clsk1indlem4  44488  limsup10exlem  46215  fourierdlem29  46579  fourierdlem56  46605  fourierswlem  46673  fouriersw  46674  nnfoctbdjlem  46898  isomenndlem  46973  hoidmvval  47020  hspmbl  47072  linc0scn0  48914  linc1  48916  lincext2  48946  blenval  49062  discsubclem  49553  discsubc  49554  iinfconstbas  49556  oppffn  49614  oppfvalg  49616