Theorem ifex 4527

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ifcif 4476

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  opex  5409  fnoe  8434  oev  8438  unxpdomlem1  9151  unxpdomlem2  9152  unxpdomlem3  9153  cantnflem1d  9589  cantnflem1  9590  ssttrcl  9616  ttrcltr  9617  ttrclselem2  9627  iunfictbso  10016  fin23lem12  10233  axcc2lem  10338  ttukeylem3  10413  pwfseqlem2  10561  pwfseqlem3  10562  xnegex  13114  xaddval  13129  xmulval  13131  seqf1olem1  13955  expval  13977  bcval  14218  ccatlen  14489  ccatvalfn  14495  ccatalpha  14508  swrdval  14558  swrd00  14559  swrd0  14573  cshfn  14704  cshnz  14706  ofccat  14883  sgnval  15002  fsumser  15644  isumless  15759  rpnnen2lem1  16130  ruclem1  16147  sadcp1  16373  smupp1  16398  gcdval  16414  eucalgval2  16499  lcmval  16510  pcval  16763  pcmpt  16811  prmreclem2  16836  prmreclem5  16839  ramub1lem2  16946  ramcl  16948  acsfn  17573  gsumvalx  18592  mulgfval  18990  mulgfvalALT  18991  mulgval  18992  mulgfn  18993  odval  19454  odf  19457  gexval  19498  frgpup3lem  19697  dprdfeq0  19944  dmdprdsplitlem  19959  abvtrivd  20756  xrsdsval  21356  uvcvval  21732  psrlidm  21908  psrridm  21909  psrascl  21925  mvrval2  21929  mplmonmul  21982  mplmon2  22007  psdmplcl  22096  coe1tmmul2fv  22211  coe1pwmulfv  22213  mat1comp  22375  mat1ov  22383  matsc  22385  mat1dimid  22409  dmatmulcl  22435  scmatscmiddistr  22443  scmatscm  22448  mdetunilem9  22555  minmar1eval  22584  symgmatr01  22589  m2cpm  22676  m2cpminvid2lem  22689  decpmatid  22705  monmatcollpw  22714  mp2pm2mplem4  22744  chmatval  22764  chfacffsupp  22791  ptcmplem2  23988  ptcmplem3  23989  iccpnfhmeo  24890  xrhmeo  24891  phtpycc  24937  pcovalg  24959  pcohtpylem  24966  ovolunlem1a  25444  ovolunlem1  25445  ovolicc1  25464  ioorval  25522  mbfmax  25597  i1f1lem  25637  itg11  25639  itg1addlem3  25646  i1fres  25653  itg1climres  25662  mbfi1fseqlem4  25666  mbfi1fseqlem6  25668  mbfi1flimlem  25670  mbfi1flim  25671  itg2uba  25691  itg2splitlem  25696  itg2monolem1  25698  itg2gt0  25708  itg2cnlem1  25709  i1fibl  25756  itgeqa  25762  itgcn  25793  ditgex  25800  dvexp3  25929  ply1nzb  26075  ig1pval  26128  elply2  26148  dvply1  26238  aareccl  26281  dvtaylp  26325  pserdvlem2  26385  abelthlem9  26397  logtayl  26616  cxpval  26620  leibpilem2  26898  leibpi  26899  lgamgulmlem4  26989  lgamgulmlem5  26990  igamval  27004  vmaval  27070  vmaf  27076  muval  27089  prmorcht  27135  pclogsum  27173  dchrinvcl  27211  dchrptlem2  27223  bposlem5  27246  lgsval  27259  lgsfval  27260  lgsdir  27290  lgsdilem2  27291  lgsdi  27292  lgsne0  27293  gausslemma2dlem1  27324  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  padicval  27575  padicabv  27588  ostth1  27591  expsval  28368  axlowdimlem15  28955  axlowdim  28960  vtxval  28999  iedgval  29000  crctcshwlkn0lem2  29810  crctcshwlkn0lem3  29811  clwlkclwwlklem2a2  29994  psgnfzto1stlem  33110  xrge0iifcv  34019  xrge0iifhom  34022  ddeval1  34319  ddeval0  34320  mrsubcv  35626  mrsubrn  35629  dfrdg2  35909  finxpreclem2  37507  finxpreclem5  37512  poimirlem2  37735  poimirlem24  37757  mblfinlem2  37771  itg2addnclem  37784  itg2addnclem2  37785  itg2addnclem3  37786  itg2addnc  37787  ftc1anclem5  37810  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  fdc  37858  renegclALT  39135  cdleme50f  40714  cdlemk40  41089  cdlemk56  41143  dihval  41404  dihf11lem  41438  mapdhval  41896  hdmap1vallem  41969  readvrec  42532  evlsbagval  42727  fsuppind  42748  flcidc  43327  cantnfub  43478  cantnfresb  43481  clsk1indlem2  44199  clsk1indlem3  44200  clsk1indlem4  44201  limsup10exlem  45932  fourierdlem29  46296  fourierdlem56  46322  fourierswlem  46390  fouriersw  46391  nnfoctbdjlem  46615  isomenndlem  46690  hoidmvval  46737  hspmbl  46789  linc0scn0  48585  linc1  48587  lincext2  48617  blenval  48733  discsubclem  49224  discsubc  49225  iinfconstbas  49227  oppffn  49285  oppfvalg  49287