Theorem ifcl 4537

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifcld  4538  ifcli  4539  ifpr  4660  suppr  9430  infpr  9463  ttukeylem3  10471  canthp1lem2  10613  xrmaxlt  13148  xrltmin  13149  xrmaxle  13150  xrlemin  13151  lemaxle  13162  z2ge  13165  ixxin  13330  uzsup  13832  expmulnbnd  14207  discr1  14211  uzin2  15318  rexanre  15320  caubnd  15332  limsupbnd2  15456  rlimcn3  15563  reccn2  15570  lo1mul  15601  rlimno1  15627  fsumsplit  15714  isumless  15818  explecnv  15838  cvgrat  15856  fprodsplit  15939  rpnnen2lem2  16190  sadadd2lem2  16427  sadcaddlem  16434  sadadd2lem  16436  sadadd3  16438  smumullem  16469  pcmpt2  16871  prmreclem4  16897  prmreclem5  16898  prmreclem6  16899  1arith  16905  ressval  17210  acsfn  17627  mplcoe3  21952  mplcoe5  21954  ordtbaslem  23082  pnfnei  23114  mnfnei  23115  uzrest  23791  fclsval  23902  blin  24316  blin2  24324  stdbdxmet  24410  nrginvrcnlem  24586  qtopbaslem  24653  metnrmlem1a  24754  metnrmlem1  24755  addcnlem  24760  evth  24865  xlebnum  24871  minveclem3b  25335  ovolicc1  25424  ismbfd  25547  mbfposr  25560  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  mbfi1flimlem  25630  itg2const  25648  itg2const2  25649  itg2splitlem  25656  itg2monolem3  25660  itg2gt0  25668  itg2cnlem1  25669  itg2cnlem2  25670  itg2cn  25671  iblre  25702  itgreval  25705  itgneg  25712  iblss  25713  itgitg1  25717  itgle  25718  itgeqa  25722  itgss3  25723  itgless  25725  iblconst  25726  itgconst  25727  ibladdlem  25728  itgaddlem2  25732  iblabslem  25736  iblabsr  25738  iblmulc2  25739  itgmulc2lem2  25741  itgsplit  25744  bddiblnc  25750  dveflem  25890  elply2  26108  ply1term  26116  plyeq0lem  26122  plypf1  26124  coe1termlem  26170  coe1term  26171  aalioulem5  26251  aalioulem6  26252  cxpcn3lem  26664  o1cxp  26892  cxp2lim  26894  cxploglim  26895  cxploglim2  26896  ftalem1  26990  ftalem2  26991  ftalem4  26993  muf  27057  chtdif  27075  ppidif  27080  prmorcht  27095  muinv  27110  chtppilim  27393  rplogsumlem2  27403  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  rpvmasum2  27430  rplogsum  27445  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  eupth2lems  30174  resvval  33308  signspval  34550  signswmnd  34555  mblfinlem2  37659  mbfposadd  37668  cnambfre  37669  itg2addnclem  37672  itg2addnc  37675  itg2gt0cn  37676  ibladdnclem  37677  itgaddnclem2  37680  iblabsnclem  37684  iblmulc2nc  37686  itgmulc2nclem2  37688  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  areaquad  43212  mullimc  45621  mullimcf  45628  addlimc  45653  limclner  45656  stoweidlem5  46010  prproropf1olem2  47509  linc0scn0  48416  linc1  48418