Theorem ifex 4539

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  opexOLD  5448  fnoe  8496  oev  8500  unxpdomlem1  9217  unxpdomlem2  9218  unxpdomlem3  9219  cantnflem1d  9658  cantnflem1  9659  ssttrcl  9685  ttrcltr  9686  ttrclselem2  9696  iunfictbso  10099  fin23lem12  10316  axcc2lem  10421  ttukeylem3  10496  pwfseqlem2  10645  pwfseqlem3  10646  xnegex  13235  xaddval  13250  xmulval  13252  seqf1olem1  14079  expval  14101  bcval  14342  ccatlen  14614  ccatvalfn  14620  ccatalpha  14633  swrdval  14683  swrd00  14684  swrd0  14698  cshfn  14829  cshnz  14831  ofccat  15008  sgnval  15127  sgndm  15135  fsumser  15783  isumless  15901  rpnnen2lem1  16271  ruclem1  16288  sadcp1  16514  smupp1  16539  gcdval  16555  eucalgval2  16640  lcmval  16651  pcval  16905  pcmpt  16953  prmreclem2  16978  prmreclem5  16981  ramub1lem2  17088  ramcl  17090  acsfn  17716  gsumvalx  18735  mulgfval  19136  mulgfvalALT  19137  mulgval  19138  mulgfn  19139  odval  19605  odf  19608  gexval  19649  frgpup3lem  19848  dprdfeq0  20095  dmdprdsplitlem  20110  abvtrivd  20916  xrsdsval  21542  uvcvval  21917  psrlidm  22092  psrridm  22093  psrascl  22109  mvrval2  22113  mplmonmul  22168  mplmon2  22193  psdmplcl  22306  coe1tmmul2fv  22420  coe1pwmulfv  22422  mat1comp  22578  mat1ov  22586  matsc  22588  mat1dimid  22612  dmatmulcl  22638  scmatscmiddistr  22646  scmatscm  22651  mdetunilem9  22758  minmar1eval  22787  symgmatr01  22792  m2cpm  22879  m2cpminvid2lem  22892  decpmatid  22908  monmatcollpw  22917  mp2pm2mplem4  22947  chmatval  22967  chfacffsupp  22994  ptcmplem2  24191  ptcmplem3  24192  iccpnfhmeo  25085  xrhmeo  25086  phtpycc  25131  pcovalg  25152  pcohtpylem  25159  ovolunlem1a  25636  ovolunlem1  25637  ovolicc1  25656  ioorval  25714  mbfmax  25789  i1f1lem  25829  itg11  25831  itg1addlem3  25838  i1fres  25845  itg1climres  25854  mbfi1fseqlem4  25858  mbfi1fseqlem6  25860  mbfi1flimlem  25862  mbfi1flim  25863  itg2uba  25883  itg2splitlem  25888  itg2monolem1  25890  itg2gt0  25900  itg2cnlem1  25901  i1fibl  25948  itgeqa  25954  itgcn  25985  ditgex  25992  dvexp3  26118  ply1nzb  26261  ig1pval  26314  elply2  26334  dvply1  26426  aareccl  26470  dvtaylp  26514  pserdvlem2  26572  abelthlem9  26584  logtayl  26806  cxpval  26810  leibpilem2  27087  leibpi  27088  lgamgulmlem4  27177  lgamgulmlem5  27178  igamval  27192  vmaval  27258  vmaf  27264  muval  27277  prmorcht  27323  pclogsum  27360  dchrinvcl  27398  dchrptlem2  27410  bposlem5  27433  lgsval  27446  lgsfval  27447  lgsdir  27477  lgsdilem2  27478  lgsdi  27479  lgsne0  27480  gausslemma2dlem1  27511  pntrlog2bndlem4  27725  pntrlog2bndlem5  27726  padicval  27762  padicabv  27775  ostth1  27778  expsval  28599  axlowdimlem15  29287  axlowdim  29292  vtxval  29331  iedgval  29332  crctcshwlkn0lem2  30141  crctcshwlkn0lem3  30142  clwlkclwwlklem2a2  30325  psgnfzto1stlem  33401  psrmonmul  33921  xrge0iifcv  34305  xrge0iifhom  34308  ddeval1  34605  ddeval0  34606  vonf1oonfo  35580  mrsubcv  35983  mrsubrn  35986  dfrdg2  36266  finxpreclem2  38017  finxpreclem5  38022  poimirlem2  38254  poimirlem24  38276  mblfinlem2  38290  itg2addnclem  38303  itg2addnclem2  38304  itg2addnclem3  38305  itg2addnc  38306  ftc1anclem5  38329  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  fdc  38377  renegclALT  39718  cdleme50f  41297  cdlemk40  41672  cdlemk56  41726  dihval  41987  dihf11lem  42021  mapdhval  42479  hdmap1vallem  42552  readvrec  43104  evlsbagval  43301  fsuppind  43305  flcidc  43880  cantnfub  44031  cantnfresb  44034  clsk1indlem2  44751  clsk1indlem3  44752  clsk1indlem4  44753  limsup10exlem  46469  fourierdlem29  46833  fourierdlem56  46859  fourierswlem  46927  fouriersw  46928  nnfoctbdjlem  47152  isomenndlem  47227  hoidmvval  47274  hspmbl  47326  linc0scn0  49186  linc1  49188  lincext2  49218  blenval  49334  discsubclem  49824  discsubc  49825  iinfconstbas  49827  oppffn  49885  oppfvalg  49887