Theorem ifcl 4522

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  ifcld  4523  ifcli  4524  ifpr  4647  suppr  9365  infpr  9398  ttukeylem3  10411  canthp1lem2  10553  xrmaxlt  13084  xrltmin  13085  xrmaxle  13086  xrlemin  13087  lemaxle  13098  z2ge  13101  ixxin  13266  uzsup  13771  expmulnbnd  14146  discr1  14150  uzin2  15256  rexanre  15258  caubnd  15270  limsupbnd2  15394  rlimcn3  15501  reccn2  15508  lo1mul  15539  rlimno1  15565  fsumsplit  15652  isumless  15756  explecnv  15776  cvgrat  15794  fprodsplit  15877  rpnnen2lem2  16128  sadadd2lem2  16365  sadcaddlem  16372  sadadd2lem  16374  sadadd3  16376  smumullem  16407  pcmpt2  16809  prmreclem4  16835  prmreclem5  16836  prmreclem6  16837  1arith  16843  ressval  17148  acsfn  17569  mplcoe3  21976  mplcoe5  21978  ordtbaslem  23106  pnfnei  23138  mnfnei  23139  uzrest  23815  fclsval  23926  blin  24339  blin2  24347  stdbdxmet  24433  nrginvrcnlem  24609  qtopbaslem  24676  metnrmlem1a  24777  metnrmlem1  24778  addcnlem  24783  evth  24888  xlebnum  24894  minveclem3b  25358  ovolicc1  25447  ismbfd  25570  mbfposr  25583  mbfi1fseqlem4  25649  mbfi1fseqlem5  25650  mbfi1flimlem  25653  itg2const  25671  itg2const2  25672  itg2splitlem  25679  itg2monolem3  25683  itg2gt0  25691  itg2cnlem1  25692  itg2cnlem2  25693  itg2cn  25694  iblre  25725  itgreval  25728  itgneg  25735  iblss  25736  itgitg1  25740  itgle  25741  itgeqa  25745  itgss3  25746  itgless  25748  iblconst  25749  itgconst  25750  ibladdlem  25751  itgaddlem2  25755  iblabslem  25759  iblabsr  25761  iblmulc2  25762  itgmulc2lem2  25764  itgsplit  25767  bddiblnc  25773  dveflem  25913  elply2  26131  ply1term  26139  plyeq0lem  26145  plypf1  26147  coe1termlem  26193  coe1term  26194  aalioulem5  26274  aalioulem6  26275  cxpcn3lem  26687  o1cxp  26915  cxp2lim  26917  cxploglim  26918  cxploglim2  26919  ftalem1  27013  ftalem2  27014  ftalem4  27016  muf  27080  chtdif  27098  ppidif  27103  prmorcht  27118  muinv  27133  chtppilim  27416  rplogsumlem2  27426  dchrvmasumiflem1  27442  dchrvmasumiflem2  27443  rpvmasum2  27453  rplogsum  27468  ostth2lem2  27575  ostth2lem3  27576  ostth2lem4  27577  eupth2lems  30222  resvval  33303  signspval  34588  signswmnd  34593  mblfinlem2  37721  mbfposadd  37730  cnambfre  37731  itg2addnclem  37734  itg2addnc  37737  itg2gt0cn  37738  ibladdnclem  37739  itgaddnclem2  37742  iblabsnclem  37746  iblmulc2nc  37748  itgmulc2nclem2  37750  ftc1anclem5  37760  ftc1anclem7  37762  ftc1anclem8  37763  areaquad  43336  mullimc  45743  mullimcf  45750  addlimc  45773  limclner  45776  stoweidlem5  46130  prproropf1olem2  47631  linc0scn0  48551  linc1  48553