Theorem ifex 4532

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  opexOLD  5420  fnoe  8447  oev  8451  unxpdomlem1  9168  unxpdomlem2  9169  unxpdomlem3  9170  cantnflem1d  9609  cantnflem1  9610  ssttrcl  9636  ttrcltr  9637  ttrclselem2  9647  iunfictbso  10036  fin23lem12  10253  axcc2lem  10358  ttukeylem3  10433  pwfseqlem2  10582  pwfseqlem3  10583  xnegex  13135  xaddval  13150  xmulval  13152  seqf1olem1  13976  expval  13998  bcval  14239  ccatlen  14510  ccatvalfn  14516  ccatalpha  14529  swrdval  14579  swrd00  14580  swrd0  14594  cshfn  14725  cshnz  14727  ofccat  14904  sgnval  15023  fsumser  15665  isumless  15780  rpnnen2lem1  16151  ruclem1  16168  sadcp1  16394  smupp1  16419  gcdval  16435  eucalgval2  16520  lcmval  16531  pcval  16784  pcmpt  16832  prmreclem2  16857  prmreclem5  16860  ramub1lem2  16967  ramcl  16969  acsfn  17594  gsumvalx  18613  mulgfval  19011  mulgfvalALT  19012  mulgval  19013  mulgfn  19014  odval  19475  odf  19478  gexval  19519  frgpup3lem  19718  dprdfeq0  19965  dmdprdsplitlem  19980  abvtrivd  20777  xrsdsval  21377  uvcvval  21753  psrlidm  21929  psrridm  21930  psrascl  21946  mvrval2  21950  mplmonmul  22003  mplmon2  22028  psdmplcl  22117  coe1tmmul2fv  22232  coe1pwmulfv  22234  mat1comp  22396  mat1ov  22404  matsc  22406  mat1dimid  22430  dmatmulcl  22456  scmatscmiddistr  22464  scmatscm  22469  mdetunilem9  22576  minmar1eval  22605  symgmatr01  22610  m2cpm  22697  m2cpminvid2lem  22710  decpmatid  22726  monmatcollpw  22735  mp2pm2mplem4  22765  chmatval  22785  chfacffsupp  22812  ptcmplem2  24009  ptcmplem3  24010  iccpnfhmeo  24911  xrhmeo  24912  phtpycc  24958  pcovalg  24980  pcohtpylem  24987  ovolunlem1a  25465  ovolunlem1  25466  ovolicc1  25485  ioorval  25543  mbfmax  25618  i1f1lem  25658  itg11  25660  itg1addlem3  25667  i1fres  25674  itg1climres  25683  mbfi1fseqlem4  25687  mbfi1fseqlem6  25689  mbfi1flimlem  25691  mbfi1flim  25692  itg2uba  25712  itg2splitlem  25717  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  i1fibl  25777  itgeqa  25783  itgcn  25814  ditgex  25821  dvexp3  25950  ply1nzb  26096  ig1pval  26149  elply2  26169  dvply1  26259  aareccl  26302  dvtaylp  26346  pserdvlem2  26406  abelthlem9  26418  logtayl  26637  cxpval  26641  leibpilem2  26919  leibpi  26920  lgamgulmlem4  27010  lgamgulmlem5  27011  igamval  27025  vmaval  27091  vmaf  27097  muval  27110  prmorcht  27156  pclogsum  27194  dchrinvcl  27232  dchrptlem2  27244  bposlem5  27267  lgsval  27280  lgsfval  27281  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  gausslemma2dlem1  27345  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  padicval  27596  padicabv  27609  ostth1  27612  expsval  28433  axlowdimlem15  29041  axlowdim  29046  vtxval  29085  iedgval  29086  crctcshwlkn0lem2  29896  crctcshwlkn0lem3  29897  clwlkclwwlklem2a2  30080  psgnfzto1stlem  33193  psrmonmul  33726  xrge0iifcv  34111  xrge0iifhom  34114  ddeval1  34411  ddeval0  34412  mrsubcv  35723  mrsubrn  35726  dfrdg2  36006  finxpreclem2  37642  finxpreclem5  37647  poimirlem2  37870  poimirlem24  37892  mblfinlem2  37906  itg2addnclem  37919  itg2addnclem2  37920  itg2addnclem3  37921  itg2addnc  37922  ftc1anclem5  37945  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  fdc  37993  renegclALT  39336  cdleme50f  40915  cdlemk40  41290  cdlemk56  41344  dihval  41605  dihf11lem  41639  mapdhval  42097  hdmap1vallem  42170  readvrec  42729  evlsbagval  42924  fsuppind  42945  flcidc  43524  cantnfub  43675  cantnfresb  43678  clsk1indlem2  44395  clsk1indlem3  44396  clsk1indlem4  44397  limsup10exlem  46127  fourierdlem29  46491  fourierdlem56  46517  fourierswlem  46585  fouriersw  46586  nnfoctbdjlem  46810  isomenndlem  46885  hoidmvval  46932  hspmbl  46984  linc0scn0  48780  linc1  48782  lincext2  48812  blenval  48928  discsubclem  49419  discsubc  49420  iinfconstbas  49422  oppffn  49480  oppfvalg  49482