Theorem ifcl 3983

Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)

Assertion

Ref	Expression
ifcl

Proof of Theorem ifcl

Step	Hyp	Ref	Expression
1		eleq1 2529	. 2
2		eleq1 2529	. 2
3	1, 2	ifboth 3977	1

Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  ifcif 3941

This theorem is referenced by:  ifcld  3984  ifpr  4077  suppr  7950  cantnfp1lem1OLD  8144  cantnfp1lem2OLD  8145  cantnfp1lem3OLD  8146  cantnflem1dOLD  8151  cantnflem1OLD  8152  ttukeylem3  8912  canthp1lem2  9052  xrmaxlt  11411  xrltmin  11412  xrmaxle  11413  xrlemin  11414  z2ge  11426  ixxin  11575  uzsup  11990  expmulnbnd  12298  discr1  12302  uzin2  13177  rexanre  13179  caubnd  13191  limsupbnd2  13306  rlimcn2  13413  reccn2  13419  lo1mul  13450  rlimno1  13476  fsumsplit  13562  isumless  13657  explecnv  13676  cvgrat  13692  fprodsplit  13770  rpnnen2lem2  13949  sadadd2lem2  14100  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  smumullem  14142  pcmpt2  14412  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  1arith  14445  ressval  14684  acsfn  15056  gsumzsplitOLD  16945  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  ordtbaslem  19689  pnfnei  19721  mnfnei  19722  uzrest  20398  fclsval  20509  blin  20924  blin2  20932  stdbdxmet  21018  nrginvrcnlem  21199  qtopbaslem  21265  metnrmlem1a  21362  metnrmlem1  21363  addcnlem  21368  evth  21459  xlebnum  21465  minveclem3b  21843  ovolicc1  21927  ismbfd  22047  mbfposr  22059  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1flimlem  22129  itg2const  22147  itg2const2  22148  itg2splitlem  22155  itg2monolem3  22159  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  iblre  22200  itgreval  22203  itgneg  22210  iblss  22211  itgitg1  22215  itgle  22216  itgeqa  22220  itgss3  22221  itgless  22223  iblconst  22224  itgconst  22225  ibladdlem  22226  itgaddlem2  22230  iblabslem  22234  iblabsr  22236  iblmulc2  22237  itgmulc2lem2  22239  itgsplit  22242  dveflem  22380  elply2  22593  ply1term  22601  plyeq0lem  22607  plypf1  22609  coe1termlem  22655  coe1term  22656  aalioulem5  22732  aalioulem6  22733  cxpcn3lem  23121  o1cxp  23304  cxp2lim  23306  cxploglim  23307  cxploglim2  23308  ftalem1  23346  ftalem2  23347  ftalem4  23349  muf  23414  chtdif  23432  ppidif  23437  prmorcht  23452  muinv  23469  chtppilim  23660  rplogsumlem2  23670  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  rpvmasum2  23697  rplogsum  23712  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  eupath2  24980  resvval  27817  signspval  28509  signswmnd  28514  mblfinlem2  30052  mbfposadd  30062  cnambfre  30063  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  ibladdnclem  30071  itgaddnclem2  30074  iblabsnclem  30078  iblmulc2nc  30080  itgmulc2nclem2  30082  bddiblnc  30085  ftc1anclem5  30094  ftc1anclem7  30096  ftc1anclem8  30097  areaquad  31184  mullimc  31622  mullimcf  31629  addlimc  31654  limclner  31657  stoweidlem5  31787  linc0scn0  33024  linc1  33026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942