Theorem ifex 4514

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

Syntax hints:   ∈ wcel 2109  Vcvv 3430  ifcif 4464

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  opex  5381  fnoe  8316  oev  8320  unxpdomlem1  8988  unxpdomlem2  8989  unxpdomlem3  8990  cantnflem1d  9407  cantnflem1  9408  ssttrcl  9434  ttrcltr  9435  ttrclselem2  9445  iunfictbso  9854  fin23lem12  10071  axcc2lem  10176  ttukeylem3  10251  pwfseqlem2  10399  pwfseqlem3  10400  xnegex  12924  xaddval  12939  xmulval  12941  seqf1olem1  13743  expval  13765  bcval  13999  ccatlen  14259  ccatlenOLD  14260  ccatvalfn  14267  ccatalpha  14279  swrdval  14337  swrd00  14338  swrd0  14352  cshfn  14484  cshnz  14486  ofccat  14661  sgnval  14780  fsumser  15423  isumless  15538  rpnnen2lem1  15904  ruclem1  15921  sadcp1  16143  smupp1  16168  gcdval  16184  eucalgval2  16267  lcmval  16278  pcval  16526  pcmpt  16574  prmreclem2  16599  prmreclem5  16602  ramub1lem2  16709  ramcl  16711  acsfn  17349  gsumvalx  18341  mulgfval  18683  mulgfvalALT  18684  mulgval  18685  mulgfn  18686  odval  19123  odf  19126  gexval  19164  frgpup3lem  19364  dprdfeq0  19606  dmdprdsplitlem  19621  abvtrivd  20081  xrsdsval  20623  uvcvval  20974  psrlidm  21153  psrridm  21154  mvrval2  21172  mplmonmul  21218  mplmon2  21250  coe1tmmul2fv  21430  coe1pwmulfv  21432  mat1comp  21570  mat1ov  21578  matsc  21580  mat1dimid  21604  dmatmulcl  21630  scmatscmiddistr  21638  scmatscm  21643  mdetunilem9  21750  minmar1eval  21779  symgmatr01  21784  m2cpm  21871  m2cpminvid2lem  21884  decpmatid  21900  monmatcollpw  21909  mp2pm2mplem4  21939  chmatval  21959  chfacffsupp  21986  ptcmplem2  23185  ptcmplem3  23186  iccpnfhmeo  24089  xrhmeo  24090  phtpycc  24135  pcovalg  24156  pcohtpylem  24163  ovolunlem1a  24641  ovolunlem1  24642  ovolicc1  24661  ioorval  24719  mbfmax  24794  i1f1lem  24834  itg11  24836  itg1addlem3  24843  i1fres  24851  itg1climres  24860  mbfi1fseqlem4  24864  mbfi1fseqlem6  24866  mbfi1flimlem  24868  mbfi1flim  24869  itg2uba  24889  itg2splitlem  24894  itg2monolem1  24896  itg2gt0  24906  itg2cnlem1  24907  i1fibl  24953  itgeqa  24959  itgcn  24990  ditgex  24997  dvexp3  25123  ply1nzb  25268  ig1pval  25318  elply2  25338  dvply1  25425  aareccl  25467  dvtaylp  25510  pserdvlem2  25568  abelthlem9  25580  logtayl  25796  cxpval  25800  leibpilem2  26072  leibpi  26073  lgamgulmlem4  26162  lgamgulmlem5  26163  igamval  26177  vmaval  26243  vmaf  26249  muval  26262  prmorcht  26308  pclogsum  26344  dchrinvcl  26382  dchrptlem2  26394  bposlem5  26417  lgsval  26430  lgsfval  26431  lgsdir  26461  lgsdilem2  26462  lgsdi  26463  lgsne0  26464  gausslemma2dlem1  26495  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  padicval  26746  padicabv  26759  ostth1  26762  axlowdimlem15  27305  axlowdim  27310  vtxval  27351  iedgval  27352  crctcshwlkn0lem2  28155  crctcshwlkn0lem3  28156  clwlkclwwlklem2a2  28336  psgnfzto1stlem  31346  xrge0iifcv  31863  xrge0iifhom  31866  ddeval1  32181  ddeval0  32182  mrsubcv  33451  mrsubrn  33454  dfrdg2  33750  finxpreclem2  35540  finxpreclem5  35545  poimirlem2  35758  poimirlem24  35780  mblfinlem2  35794  itg2addnclem  35807  itg2addnclem2  35808  itg2addnclem3  35809  itg2addnc  35810  ftc1anclem5  35833  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837  fdc  35882  renegclALT  36956  cdleme50f  38535  cdlemk40  38910  cdlemk56  38964  dihval  39225  dihf11lem  39259  mapdhval  39717  hdmap1vallem  39790  evlsbagval  40255  fsuppind  40259  mhphf  40265  flcidc  40979  clsk1indlem2  41605  clsk1indlem3  41606  clsk1indlem4  41607  limsup10exlem  43267  fourierdlem29  43631  fourierdlem56  43657  fourierswlem  43725  fouriersw  43726  nnfoctbdjlem  43947  isomenndlem  44022  hoidmvval  44069  hspmbl  44121  linc0scn0  45716  linc1  45718  lincext2  45748  blenval  45869