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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ifcif 4489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4490

This theorem is referenced by:  opexOLD  5444  fnoe  8491  oev  8495  unxpdomlem1  9212  unxpdomlem2  9213  unxpdomlem3  9214  cantnflem1d  9653  cantnflem1  9654  ssttrcl  9680  ttrcltr  9681  ttrclselem2  9691  iunfictbso  10094  fin23lem12  10311  axcc2lem  10416  ttukeylem3  10491  pwfseqlem2  10640  pwfseqlem3  10641  xnegex  13230  xaddval  13245  xmulval  13247  seqf1olem1  14073  expval  14095  bcval  14336  ccatlen  14608  ccatvalfn  14614  ccatalpha  14627  swrdval  14677  swrd00  14678  swrd0  14692  cshfn  14823  cshnz  14825  ofccat  15002  sgnval  15121  sgndm  15129  fsumser  15777  isumless  15895  rpnnen2lem1  16266  ruclem1  16283  sadcp1  16509  smupp1  16534  gcdval  16550  eucalgval2  16635  lcmval  16646  pcval  16900  pcmpt  16948  prmreclem2  16973  prmreclem5  16976  ramub1lem2  17083  ramcl  17085  acsfn  17711  gsumvalx  18730  mulgfval  19131  mulgfvalALT  19132  mulgval  19133  mulgfn  19134  odval  19600  odf  19603  gexval  19644  frgpup3lem  19843  dprdfeq0  20090  dmdprdsplitlem  20105  abvtrivd  20909  xrsdsval  21526  uvcvval  21901  psrlidm  22076  psrridm  22077  psrascl  22093  mvrval2  22097  mplmonmul  22152  mplmon2  22177  psdmplcl  22290  coe1tmmul2fv  22404  coe1pwmulfv  22406  mat1comp  22562  mat1ov  22570  matsc  22572  mat1dimid  22596  dmatmulcl  22622  scmatscmiddistr  22630  scmatscm  22635  mdetunilem9  22742  minmar1eval  22771  symgmatr01  22776  m2cpm  22863  m2cpminvid2lem  22876  decpmatid  22892  monmatcollpw  22901  mp2pm2mplem4  22931  chmatval  22951  chfacffsupp  22978  ptcmplem2  24175  ptcmplem3  24176  iccpnfhmeo  25069  xrhmeo  25070  phtpycc  25115  pcovalg  25136  pcohtpylem  25143  ovolunlem1a  25620  ovolunlem1  25621  ovolicc1  25640  ioorval  25698  mbfmax  25773  i1f1lem  25813  itg11  25815  itg1addlem3  25822  i1fres  25829  itg1climres  25838  mbfi1fseqlem4  25842  mbfi1fseqlem6  25844  mbfi1flimlem  25846  mbfi1flim  25847  itg2uba  25867  itg2splitlem  25872  itg2monolem1  25874  itg2gt0  25884  itg2cnlem1  25885  i1fibl  25932  itgeqa  25938  itgcn  25969  ditgex  25976  dvexp3  26102  ply1nzb  26245  ig1pval  26298  elply2  26318  dvply1  26410  aareccl  26452  dvtaylp  26495  pserdvlem2  26553  abelthlem9  26565  logtayl  26787  cxpval  26791  leibpilem2  27068  leibpi  27069  lgamgulmlem4  27158  lgamgulmlem5  27159  igamval  27173  vmaval  27239  vmaf  27245  muval  27258  prmorcht  27304  pclogsum  27341  dchrinvcl  27379  dchrptlem2  27391  bposlem5  27414  lgsval  27427  lgsfval  27428  lgsdir  27458  lgsdilem2  27459  lgsdi  27460  lgsne0  27461  gausslemma2dlem1  27492  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  padicval  27743  padicabv  27756  ostth1  27759  expsval  28580  axlowdimlem15  29243  axlowdim  29248  vtxval  29287  iedgval  29288  crctcshwlkn0lem2  30097  crctcshwlkn0lem3  30098  clwlkclwwlklem2a2  30281  psgnfzto1stlem  33357  psrmonmul  33881  xrge0iifcv  34265  xrge0iifhom  34268  ddeval1  34565  ddeval0  34566  vonf1oonfo  35494  mrsubcv  35897  mrsubrn  35900  dfrdg2  36180  finxpreclem2  37919  finxpreclem5  37924  poimirlem2  38156  poimirlem24  38178  mblfinlem2  38192  itg2addnclem  38205  itg2addnclem2  38206  itg2addnclem3  38207  itg2addnc  38208  ftc1anclem5  38231  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  fdc  38279  renegclALT  39622  cdleme50f  41201  cdlemk40  41576  cdlemk56  41630  dihval  41891  dihf11lem  41925  mapdhval  42383  hdmap1vallem  42456  readvrec  43006  evlsbagval  43203  fsuppind  43207  flcidc  43782  cantnfub  43933  cantnfresb  43936  clsk1indlem2  44653  clsk1indlem3  44654  clsk1indlem4  44655  limsup10exlem  46371  fourierdlem29  46735  fourierdlem56  46761  fourierswlem  46829  fouriersw  46830  nnfoctbdjlem  47054  isomenndlem  47129  hoidmvval  47176  hspmbl  47228  linc0scn0  49081  linc1  49083  lincext2  49113  blenval  49229  discsubclem  49719  discsubc  49720  iinfconstbas  49722  oppffn  49780  oppfvalg  49782