Theorem ifcl 4536

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ifcif 4490

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4491

This theorem is used by:  ifcld  4537  ifcli  4538  ifpr  4662  suppr  9434  infpr  9467  ttukeylem3  10505  canthp1lem2  10648  xrmaxlt  13217  xrltmin  13218  xrmaxle  13219  xrlemin  13220  lemaxle  13231  z2ge  13234  ixxin  13399  uzsup  13907  expmulnbnd  14282  discr1  14286  uzin2  15407  rexanre  15409  caubnd  15421  limsupbnd2  15545  rlimcn3  15652  reccn2  15659  lo1mul  15690  rlimno1  15716  fsumsplit  15803  isumless  15910  explecnv  15930  cvgrat  15948  fprodsplit  16031  rpnnen2lem2  16281  sadadd2lem2  16518  sadcaddlem  16525  sadadd2lem  16527  sadadd3  16529  smumullem  16560  pcmpt2  16963  prmreclem4  16989  prmreclem5  16990  prmreclem6  16991  1arith  16997  ressval  17303  acsfn  17725  mplcoe3  22204  mplcoe5  22206  ordtbaslem  23360  pnfnei  23392  mnfnei  23393  uzrest  24069  fclsval  24180  blin  24593  blin2  24601  stdbdxmet  24687  nrginvrcnlem  24863  qtopbaslem  24930  metnrmlem1a  25031  metnrmlem1  25032  addcnlem  25037  evth  25133  xlebnum  25139  minveclem3b  25602  ovolicc1  25690  ismbfd  25813  mbfposr  25826  mbfi1fseqlem4  25892  mbfi1fseqlem5  25893  mbfi1flimlem  25896  itg2const  25914  itg2const2  25915  itg2splitlem  25922  itg2monolem3  25926  itg2gt0  25934  itg2cnlem1  25935  itg2cnlem2  25936  itg2cn  25937  iblre  25968  itgreval  25971  itgneg  25978  iblss  25979  itgitg1  25983  itgle  25984  itgeqa  25988  itgss3  25989  itgless  25991  iblconst  25992  itgconst  25993  ibladdlem  25994  itgaddlem2  25998  iblabslem  26002  iblabsr  26004  iblmulc2  26005  itgmulc2lem2  26007  itgsplit  26010  bddiblnc  26016  dveflem  26153  elply2  26368  ply1term  26376  plyeq0lem  26382  plypf1  26384  coe1termlem  26430  coe1term  26431  aalioulem5  26514  aalioulem6  26515  cxpcn3lem  26927  o1cxp  27154  cxp2lim  27156  cxploglim  27157  cxploglim2  27158  ftalem1  27252  ftalem2  27253  ftalem4  27255  muf  27319  chtdif  27337  ppidif  27342  prmorcht  27357  muinv  27372  chtppilim  27654  rplogsumlem2  27664  dchrvmasumiflem1  27680  dchrvmasumiflem2  27681  rpvmasum2  27691  rplogsum  27706  ostth2lem2  27813  ostth2lem3  27814  ostth2lem4  27815  eupth2lems  30604  resvval  33662  signspval  34952  signswmnd  34957  mblfinlem2  38341  mbfposadd  38350  cnambfre  38351  itg2addnclem  38354  itg2addnc  38357  itg2gt0cn  38358  ibladdnclem  38359  itgaddnclem2  38362  iblabsnclem  38366  iblmulc2nc  38368  itgmulc2nclem2  38370  ftc1anclem5  38380  ftc1anclem7  38382  ftc1anclem8  38383  areaquad  43975  mullimc  46364  mullimcf  46371  addlimc  46394  limclner  46397  stoweidlem5  46751  prproropf1olem2  48285  linc0scn0  49235  linc1  49237