Theorem ifcl 4527

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  ifcld  4528  ifcli  4529  ifpr  4652  suppr  9387  infpr  9420  ttukeylem3  10433  canthp1lem2  10576  xrmaxlt  13108  xrltmin  13109  xrmaxle  13110  xrlemin  13111  lemaxle  13122  z2ge  13125  ixxin  13290  uzsup  13795  expmulnbnd  14170  discr1  14174  uzin2  15280  rexanre  15282  caubnd  15294  limsupbnd2  15418  rlimcn3  15525  reccn2  15532  lo1mul  15563  rlimno1  15589  fsumsplit  15676  isumless  15780  explecnv  15800  cvgrat  15818  fprodsplit  15901  rpnnen2lem2  16152  sadadd2lem2  16389  sadcaddlem  16396  sadadd2lem  16398  sadadd3  16400  smumullem  16431  pcmpt2  16833  prmreclem4  16859  prmreclem5  16860  prmreclem6  16861  1arith  16867  ressval  17172  acsfn  17594  mplcoe3  22005  mplcoe5  22007  ordtbaslem  23144  pnfnei  23176  mnfnei  23177  uzrest  23853  fclsval  23964  blin  24377  blin2  24385  stdbdxmet  24471  nrginvrcnlem  24647  qtopbaslem  24714  metnrmlem1a  24815  metnrmlem1  24816  addcnlem  24821  evth  24926  xlebnum  24932  minveclem3b  25396  ovolicc1  25485  ismbfd  25608  mbfposr  25621  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1flimlem  25691  itg2const  25709  itg2const2  25710  itg2splitlem  25717  itg2monolem3  25721  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  itg2cn  25732  iblre  25763  itgreval  25766  itgneg  25773  iblss  25774  itgitg1  25778  itgle  25779  itgeqa  25783  itgss3  25784  itgless  25786  iblconst  25787  itgconst  25788  ibladdlem  25789  itgaddlem2  25793  iblabslem  25797  iblabsr  25799  iblmulc2  25800  itgmulc2lem2  25802  itgsplit  25805  bddiblnc  25811  dveflem  25951  elply2  26169  ply1term  26177  plyeq0lem  26183  plypf1  26185  coe1termlem  26231  coe1term  26232  aalioulem5  26312  aalioulem6  26313  cxpcn3lem  26725  o1cxp  26953  cxp2lim  26955  cxploglim  26956  cxploglim2  26957  ftalem1  27051  ftalem2  27052  ftalem4  27054  muf  27118  chtdif  27136  ppidif  27141  prmorcht  27156  muinv  27171  chtppilim  27454  rplogsumlem2  27464  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  rpvmasum2  27491  rplogsum  27506  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  eupth2lems  30325  resvval  33421  signspval  34729  signswmnd  34734  mblfinlem2  37906  mbfposadd  37915  cnambfre  37916  itg2addnclem  37919  itg2addnc  37922  itg2gt0cn  37923  ibladdnclem  37924  itgaddnclem2  37927  iblabsnclem  37931  iblmulc2nc  37933  itgmulc2nclem2  37935  ftc1anclem5  37945  ftc1anclem7  37947  ftc1anclem8  37948  areaquad  43570  mullimc  45973  mullimcf  45980  addlimc  46003  limclner  46006  stoweidlem5  46360  prproropf1olem2  47861  linc0scn0  48780  linc1  48782