Theorem ifcl 4528

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  ifcld  4529  ifcli  4530  ifpr  4654  suppr  9448  infpr  9481  ttukeylem3  10570  canthp1lem2  10719  xrmaxlt  13292  xrltmin  13293  xrmaxle  13294  xrlemin  13295  lemaxle  13306  z2ge  13309  ixxin  13474  uzsup  13983  expmulnbnd  14359  discr1  14363  uzin2  15492  rexanre  15494  caubnd  15506  limsupbnd2  15630  rlimcn3  15737  reccn2  15744  lo1mul  15775  rlimno1  15801  fsumsplit  15887  isumless  15994  explecnv  16014  cvgrat  16032  fprodsplit  16113  rpnnen2lem2  16363  sadadd2lem2  16600  sadcaddlem  16607  sadadd2lem  16609  sadadd3  16611  smumullem  16642  pcmpt2  17051  prmreclem4  17077  prmreclem5  17078  prmreclem6  17079  1arith  17085  ressval  17391  acsfn  17813  mplcoe3  22327  mplcoe5  22329  ordtbaslem  23486  pnfnei  23518  mnfnei  23519  uzrest  24196  fclsval  24307  blin  24720  blin2  24728  stdbdxmet  24814  nrginvrcnlem  24990  qtopbaslem  25057  metnrmlem1a  25158  metnrmlem1  25159  addcnlem  25164  evth  25260  xlebnum  25266  minveclem3b  25729  ovolicc1  25817  ismbfd  25940  mbfposr  25953  mbfi1fseqlem4  26019  mbfi1fseqlem5  26020  mbfi1flimlem  26023  itg2const  26041  itg2const2  26042  itg2splitlem  26049  itg2monolem3  26053  itg2gt0  26061  itg2cnlem1  26062  itg2cnlem2  26063  itg2cn  26064  iblre  26094  itgreval  26097  itgneg  26104  iblss  26105  itgitg1  26109  itgle  26110  itgeqa  26114  itgss3  26115  itgless  26117  iblconst  26118  itgconst  26119  ibladdlem  26120  itgaddlem2  26124  iblabslem  26128  iblabsr  26130  iblmulc2  26131  itgmulc2lem2  26133  itgsplit  26136  bddiblnc  26142  dveflem  26279  elply2  26494  ply1term  26502  plyeq0lem  26509  plypf1  26511  coe1termlem  26557  coe1term  26558  aalioulem5  26645  aalioulem6  26646  cxpcn3lem  27057  o1cxp  27284  cxp2lim  27286  cxploglim  27287  cxploglim2  27288  ftalem1  27382  ftalem2  27383  ftalem4  27385  muf  27449  chtdif  27467  ppidif  27472  prmorcht  27487  muinv  27502  chtppilim  27784  rplogsumlem2  27794  dchrvmasumiflem1  27810  dchrvmasumiflem2  27811  rpvmasum2  27821  rplogsum  27836  ostth2lem2  27943  ostth2lem3  27944  ostth2lem4  27945  eupth2lems  30821  resvval  33872  signspval  35164  signswmnd  35169  mblfinlem2  38544  mbfposadd  38553  cnambfre  38554  itg2addnclem  38557  itg2addnc  38560  itg2gt0cn  38561  ibladdnclem  38562  itgaddnclem2  38565  iblabsnclem  38569  iblmulc2nc  38571  itgmulc2nclem2  38573  ftc1anclem5  38583  ftc1anclem7  38585  ftc1anclem8  38586  areaquad  44176  mullimc  46572  mullimcf  46579  addlimc  46602  limclner  46605  stoweidlem5  46959  prproropf1olem2  48530  linc0scn0  49479  linc1  49481