Theorem ifcl 4431

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2083  ifcif 4387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1766  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-if 4388

This theorem is referenced by:  ifcld  4432  ifcli  4433  ifexg  4434  ifpr  4542  suppr  8788  infpr  8820  ttukeylem3  9786  canthp1lem2  9928  xrmaxlt  12428  xrltmin  12429  xrmaxle  12430  xrlemin  12431  lemaxle  12442  z2ge  12445  ixxin  12609  uzsup  13085  expmulnbnd  13450  discr1  13454  uzin2  14542  rexanre  14544  caubnd  14556  limsupbnd2  14678  rlimcn2  14785  reccn2  14791  lo1mul  14822  rlimno1  14848  fsumsplit  14934  isumless  15037  explecnv  15057  cvgrat  15076  fprodsplit  15157  rpnnen2lem2  15405  sadadd2lem2  15636  sadcaddlem  15643  sadadd2lem  15645  sadadd3  15647  smumullem  15678  pcmpt2  16062  prmreclem4  16088  prmreclem5  16089  prmreclem6  16090  1arith  16096  ressval  16384  acsfn  16763  mplcoe3  19938  mplcoe5  19940  ordtbaslem  21484  pnfnei  21516  mnfnei  21517  uzrest  22193  fclsval  22304  blin  22718  blin2  22726  stdbdxmet  22812  nrginvrcnlem  22987  qtopbaslem  23054  metnrmlem1a  23153  metnrmlem1  23154  addcnlem  23159  evth  23250  xlebnum  23256  minveclem3b  23718  ovolicc1  23804  ismbfd  23927  mbfposr  23940  mbfi1fseqlem4  24006  mbfi1fseqlem5  24007  mbfi1flimlem  24010  itg2const  24028  itg2const2  24029  itg2splitlem  24036  itg2monolem3  24040  itg2gt0  24048  itg2cnlem1  24049  itg2cnlem2  24050  itg2cn  24051  iblre  24081  itgreval  24084  itgneg  24091  iblss  24092  itgitg1  24096  itgle  24097  itgeqa  24101  itgss3  24102  itgless  24104  iblconst  24105  itgconst  24106  ibladdlem  24107  itgaddlem2  24111  iblabslem  24115  iblabsr  24117  iblmulc2  24118  itgmulc2lem2  24120  itgsplit  24123  dveflem  24263  elply2  24473  ply1term  24481  plyeq0lem  24487  plypf1  24489  coe1termlem  24535  coe1term  24536  aalioulem5  24612  aalioulem6  24613  cxpcn3lem  25013  o1cxp  25238  cxp2lim  25240  cxploglim  25241  cxploglim2  25242  ftalem1  25336  ftalem2  25337  ftalem4  25339  muf  25403  chtdif  25421  ppidif  25426  prmorcht  25441  muinv  25456  chtppilim  25737  rplogsumlem2  25747  dchrvmasumiflem1  25763  dchrvmasumiflem2  25764  rpvmasum2  25774  rplogsum  25789  ostth2lem2  25896  ostth2lem3  25897  ostth2lem4  25898  eupth2lems  27703  resvval  30550  signspval  31435  signswmnd  31440  mblfinlem2  34482  mbfposadd  34491  cnambfre  34492  itg2addnclem  34495  itg2addnc  34498  itg2gt0cn  34499  ibladdnclem  34500  itgaddnclem2  34503  iblabsnclem  34507  iblmulc2nc  34509  itgmulc2nclem2  34511  bddiblnc  34514  ftc1anclem5  34523  ftc1anclem7  34525  ftc1anclem8  34526  areaquad  39329  mullimc  41460  mullimcf  41467  addlimc  41492  limclner  41495  stoweidlem5  41854  prproropf1olem2  43170  linc0scn0  43980  linc1  43982