Theorem ifcl 4525

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 2824	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2824	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3	1, 2	ifboth 4519	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  ifcld  4526  ifcli  4527  ifpr  4650  suppr  9375  infpr  9408  ttukeylem3  10421  canthp1lem2  10564  xrmaxlt  13096  xrltmin  13097  xrmaxle  13098  xrlemin  13099  lemaxle  13110  z2ge  13113  ixxin  13278  uzsup  13783  expmulnbnd  14158  discr1  14162  uzin2  15268  rexanre  15270  caubnd  15282  limsupbnd2  15406  rlimcn3  15513  reccn2  15520  lo1mul  15551  rlimno1  15577  fsumsplit  15664  isumless  15768  explecnv  15788  cvgrat  15806  fprodsplit  15889  rpnnen2lem2  16140  sadadd2lem2  16377  sadcaddlem  16384  sadadd2lem  16386  sadadd3  16388  smumullem  16419  pcmpt2  16821  prmreclem4  16847  prmreclem5  16848  prmreclem6  16849  1arith  16855  ressval  17160  acsfn  17582  mplcoe3  21993  mplcoe5  21995  ordtbaslem  23132  pnfnei  23164  mnfnei  23165  uzrest  23841  fclsval  23952  blin  24365  blin2  24373  stdbdxmet  24459  nrginvrcnlem  24635  qtopbaslem  24702  metnrmlem1a  24803  metnrmlem1  24804  addcnlem  24809  evth  24914  xlebnum  24920  minveclem3b  25384  ovolicc1  25473  ismbfd  25596  mbfposr  25609  mbfi1fseqlem4  25675  mbfi1fseqlem5  25676  mbfi1flimlem  25679  itg2const  25697  itg2const2  25698  itg2splitlem  25705  itg2monolem3  25709  itg2gt0  25717  itg2cnlem1  25718  itg2cnlem2  25719  itg2cn  25720  iblre  25751  itgreval  25754  itgneg  25761  iblss  25762  itgitg1  25766  itgle  25767  itgeqa  25771  itgss3  25772  itgless  25774  iblconst  25775  itgconst  25776  ibladdlem  25777  itgaddlem2  25781  iblabslem  25785  iblabsr  25787  iblmulc2  25788  itgmulc2lem2  25790  itgsplit  25793  bddiblnc  25799  dveflem  25939  elply2  26157  ply1term  26165  plyeq0lem  26171  plypf1  26173  coe1termlem  26219  coe1term  26220  aalioulem5  26300  aalioulem6  26301  cxpcn3lem  26713  o1cxp  26941  cxp2lim  26943  cxploglim  26944  cxploglim2  26945  ftalem1  27039  ftalem2  27040  ftalem4  27042  muf  27106  chtdif  27124  ppidif  27129  prmorcht  27144  muinv  27159  chtppilim  27442  rplogsumlem2  27452  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  rpvmasum2  27479  rplogsum  27494  ostth2lem2  27601  ostth2lem3  27602  ostth2lem4  27603  eupth2lems  30313  resvval  33410  signspval  34709  signswmnd  34714  mblfinlem2  37859  mbfposadd  37868  cnambfre  37869  itg2addnclem  37872  itg2addnc  37875  itg2gt0cn  37876  ibladdnclem  37877  itgaddnclem2  37880  iblabsnclem  37884  iblmulc2nc  37886  itgmulc2nclem2  37888  ftc1anclem5  37898  ftc1anclem7  37900  ftc1anclem8  37901  areaquad  43458  mullimc  45862  mullimcf  45869  addlimc  45892  limclner  45895  stoweidlem5  46249  prproropf1olem2  47750  linc0scn0  48669  linc1  48671