Theorem ifex 4528

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  opexOLD  5429  fnoe  8473  oev  8477  unxpdomlem1  9194  unxpdomlem2  9195  unxpdomlem3  9196  cantnflem1d  9637  cantnflem1  9638  ssttrcl  9664  ttrcltr  9665  ttrclselem2  9675  iunfictbso  10064  fin23lem12  10282  axcc2lem  10387  ttukeylem3  10462  pwfseqlem2  10611  pwfseqlem3  10612  xnegex  13205  xaddval  13220  xmulval  13222  seqf1olem1  14048  expval  14070  bcval  14311  ccatlen  14582  ccatvalfn  14588  ccatalpha  14601  swrdval  14651  swrd00  14652  swrd0  14666  cshfn  14797  cshnz  14799  ofccat  14976  sgnval  15095  fsumser  15748  isumless  15866  rpnnen2lem1  16237  ruclem1  16254  sadcp1  16480  smupp1  16505  gcdval  16521  eucalgval2  16606  lcmval  16617  pcval  16871  pcmpt  16919  prmreclem2  16944  prmreclem5  16947  ramub1lem2  17054  ramcl  17056  acsfn  17682  gsumvalx  18701  mulgfval  19102  mulgfvalALT  19103  mulgval  19104  mulgfn  19105  odval  19565  odf  19568  gexval  19609  frgpup3lem  19808  dprdfeq0  20055  dmdprdsplitlem  20070  abvtrivd  20869  xrsdsval  21451  uvcvval  21826  psrlidm  22001  psrridm  22002  psrascl  22018  mvrval2  22022  mplmonmul  22077  mplmon2  22102  psdmplcl  22215  coe1tmmul2fv  22329  coe1pwmulfv  22331  mat1comp  22488  mat1ov  22496  matsc  22498  mat1dimid  22522  dmatmulcl  22548  scmatscmiddistr  22556  scmatscm  22561  mdetunilem9  22668  minmar1eval  22697  symgmatr01  22702  m2cpm  22789  m2cpminvid2lem  22802  decpmatid  22818  monmatcollpw  22827  mp2pm2mplem4  22857  chmatval  22877  chfacffsupp  22904  ptcmplem2  24101  ptcmplem3  24102  iccpnfhmeo  24995  xrhmeo  24996  phtpycc  25041  pcovalg  25062  pcohtpylem  25069  ovolunlem1a  25546  ovolunlem1  25547  ovolicc1  25566  ioorval  25624  mbfmax  25699  i1f1lem  25739  itg11  25741  itg1addlem3  25748  i1fres  25755  itg1climres  25764  mbfi1fseqlem4  25768  mbfi1fseqlem6  25770  mbfi1flimlem  25772  mbfi1flim  25773  itg2uba  25793  itg2splitlem  25798  itg2monolem1  25800  itg2gt0  25810  itg2cnlem1  25811  i1fibl  25858  itgeqa  25864  itgcn  25895  ditgex  25902  dvexp3  26028  ply1nzb  26171  ig1pval  26224  elply2  26244  dvply1  26336  aareccl  26378  dvtaylp  26421  pserdvlem2  26479  abelthlem9  26491  logtayl  26713  cxpval  26717  leibpilem2  26994  leibpi  26995  lgamgulmlem4  27084  lgamgulmlem5  27085  igamval  27099  vmaval  27165  vmaf  27171  muval  27184  prmorcht  27230  pclogsum  27267  dchrinvcl  27305  dchrptlem2  27317  bposlem5  27340  lgsval  27353  lgsfval  27354  lgsdir  27384  lgsdilem2  27385  lgsdi  27386  lgsne0  27387  gausslemma2dlem1  27418  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  padicval  27669  padicabv  27682  ostth1  27685  expsval  28506  axlowdimlem15  29114  axlowdim  29119  vtxval  29158  iedgval  29159  crctcshwlkn0lem2  29968  crctcshwlkn0lem3  29969  clwlkclwwlklem2a2  30152  psgnfzto1stlem  33241  psrmonmul  33808  xrge0iifcv  34192  xrge0iifhom  34195  ddeval1  34492  ddeval0  34493  vonf1oonfo  35419  mrsubcv  35821  mrsubrn  35824  dfrdg2  36104  finxpreclem2  37845  finxpreclem5  37850  poimirlem2  38082  poimirlem24  38104  mblfinlem2  38118  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  itg2addnc  38134  ftc1anclem5  38157  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  fdc  38205  renegclALT  39548  cdleme50f  41127  cdlemk40  41502  cdlemk56  41556  dihval  41817  dihf11lem  41851  mapdhval  42309  hdmap1vallem  42382  readvrec  42932  evlsbagval  43129  fsuppind  43133  flcidc  43708  cantnfub  43859  cantnfresb  43862  clsk1indlem2  44579  clsk1indlem3  44580  clsk1indlem4  44581  limsup10exlem  46307  fourierdlem29  46671  fourierdlem56  46697  fourierswlem  46765  fouriersw  46766  nnfoctbdjlem  46990  isomenndlem  47065  hoidmvval  47112  hspmbl  47164  linc0scn0  49006  linc1  49008  lincext2  49038  blenval  49154  discsubclem  49645  discsubc  49646  iinfconstbas  49648  oppffn  49706  oppfvalg  49708