Theorem ifcl 4529

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

Assertion

Ref	Expression
ifcl	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcl

Step	Hyp	Ref	Expression
1		eleq1 2853	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2853	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3	1, 2	ifboth 4523	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  ifcld  4530  ifcli  4531  ifpr  4655  suppr  9420  infpr  9453  ttukeylem3  10483  canthp1lem2  10626  xrmaxlt  13195  xrltmin  13196  xrmaxle  13197  xrlemin  13198  lemaxle  13209  z2ge  13212  ixxin  13377  uzsup  13884  expmulnbnd  14259  discr1  14263  uzin2  15384  rexanre  15386  caubnd  15398  limsupbnd2  15522  rlimcn3  15629  reccn2  15636  lo1mul  15667  rlimno1  15693  fsumsplit  15780  isumless  15887  explecnv  15907  cvgrat  15925  fprodsplit  16008  rpnnen2lem2  16259  sadadd2lem2  16496  sadcaddlem  16503  sadadd2lem  16505  sadadd3  16507  smumullem  16538  pcmpt2  16941  prmreclem4  16967  prmreclem5  16968  prmreclem6  16969  1arith  16975  ressval  17281  acsfn  17703  mplcoe3  22146  mplcoe5  22148  ordtbaslem  23302  pnfnei  23334  mnfnei  23335  uzrest  24011  fclsval  24122  blin  24535  blin2  24543  stdbdxmet  24629  nrginvrcnlem  24805  qtopbaslem  24872  metnrmlem1a  24973  metnrmlem1  24974  addcnlem  24979  evth  25075  xlebnum  25081  minveclem3b  25544  ovolicc1  25632  ismbfd  25755  mbfposr  25768  mbfi1fseqlem4  25834  mbfi1fseqlem5  25835  mbfi1flimlem  25838  itg2const  25856  itg2const2  25857  itg2splitlem  25864  itg2monolem3  25868  itg2gt0  25876  itg2cnlem1  25877  itg2cnlem2  25878  itg2cn  25879  iblre  25910  itgreval  25913  itgneg  25920  iblss  25921  itgitg1  25925  itgle  25926  itgeqa  25930  itgss3  25931  itgless  25933  iblconst  25934  itgconst  25935  ibladdlem  25936  itgaddlem2  25940  iblabslem  25944  iblabsr  25946  iblmulc2  25947  itgmulc2lem2  25949  itgsplit  25952  bddiblnc  25958  dveflem  26095  elply2  26310  ply1term  26318  plyeq0lem  26324  plypf1  26326  coe1termlem  26372  coe1term  26373  aalioulem5  26454  aalioulem6  26455  cxpcn3lem  26866  o1cxp  27093  cxp2lim  27095  cxploglim  27096  cxploglim2  27097  ftalem1  27191  ftalem2  27192  ftalem4  27194  muf  27258  chtdif  27276  ppidif  27281  prmorcht  27296  muinv  27311  chtppilim  27593  rplogsumlem2  27603  dchrvmasumiflem1  27619  dchrvmasumiflem2  27620  rpvmasum2  27630  rplogsum  27645  ostth2lem2  27752  ostth2lem3  27753  ostth2lem4  27754  eupth2lems  30494  resvval  33559  signspval  34851  signswmnd  34856  mblfinlem2  38164  mbfposadd  38173  cnambfre  38174  itg2addnclem  38177  itg2addnc  38180  itg2gt0cn  38181  ibladdnclem  38182  itgaddnclem2  38185  iblabsnclem  38189  iblmulc2nc  38191  itgmulc2nclem2  38193  ftc1anclem5  38203  ftc1anclem7  38205  ftc1anclem8  38206  areaquad  43800  mullimc  46191  mullimcf  46198  addlimc  46221  limclner  46224  stoweidlem5  46578  prproropf1olem2  48109  linc0scn0  49055  linc1  49057