Theorem ifcl 4538

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 4532	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

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

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 4493

This theorem is used by:  ifcld  4539  ifcli  4540  ifpr  4664  suppr  9442  infpr  9475  ttukeylem3  10513  canthp1lem2  10656  xrmaxlt  13225  xrltmin  13226  xrmaxle  13227  xrlemin  13228  lemaxle  13239  z2ge  13242  ixxin  13407  uzsup  13916  expmulnbnd  14291  discr1  14295  uzin2  15422  rexanre  15424  caubnd  15436  limsupbnd2  15560  rlimcn3  15667  reccn2  15674  lo1mul  15705  rlimno1  15731  fsumsplit  15818  isumless  15925  explecnv  15945  cvgrat  15963  fprodsplit  16046  rpnnen2lem2  16296  sadadd2lem2  16533  sadcaddlem  16540  sadadd2lem  16542  sadadd3  16544  smumullem  16575  pcmpt2  16978  prmreclem4  17004  prmreclem5  17005  prmreclem6  17006  1arith  17012  ressval  17318  acsfn  17740  mplcoe3  22226  mplcoe5  22228  ordtbaslem  23382  pnfnei  23414  mnfnei  23415  uzrest  24091  fclsval  24202  blin  24615  blin2  24623  stdbdxmet  24709  nrginvrcnlem  24885  qtopbaslem  24952  metnrmlem1a  25053  metnrmlem1  25054  addcnlem  25059  evth  25155  xlebnum  25161  minveclem3b  25624  ovolicc1  25712  ismbfd  25835  mbfposr  25848  mbfi1fseqlem4  25914  mbfi1fseqlem5  25915  mbfi1flimlem  25918  itg2const  25936  itg2const2  25937  itg2splitlem  25944  itg2monolem3  25948  itg2gt0  25956  itg2cnlem1  25957  itg2cnlem2  25958  itg2cn  25959  iblre  25990  itgreval  25993  itgneg  26000  iblss  26001  itgitg1  26005  itgle  26006  itgeqa  26010  itgss3  26011  itgless  26013  iblconst  26014  itgconst  26015  ibladdlem  26016  itgaddlem2  26020  iblabslem  26024  iblabsr  26026  iblmulc2  26027  itgmulc2lem2  26029  itgsplit  26032  bddiblnc  26038  dveflem  26175  elply2  26390  ply1term  26398  plyeq0lem  26404  plypf1  26406  coe1termlem  26452  coe1term  26453  aalioulem5  26536  aalioulem6  26537  cxpcn3lem  26949  o1cxp  27176  cxp2lim  27178  cxploglim  27179  cxploglim2  27180  ftalem1  27274  ftalem2  27275  ftalem4  27277  muf  27341  chtdif  27359  ppidif  27364  prmorcht  27379  muinv  27394  chtppilim  27676  rplogsumlem2  27686  dchrvmasumiflem1  27702  dchrvmasumiflem2  27703  rpvmasum2  27713  rplogsum  27728  ostth2lem2  27835  ostth2lem3  27836  ostth2lem4  27837  eupth2lems  30626  resvval  33680  signspval  34971  signswmnd  34976  mblfinlem2  38350  mbfposadd  38359  cnambfre  38360  itg2addnclem  38363  itg2addnc  38366  itg2gt0cn  38367  ibladdnclem  38368  itgaddnclem2  38371  iblabsnclem  38375  iblmulc2nc  38377  itgmulc2nclem2  38379  ftc1anclem5  38389  ftc1anclem7  38391  ftc1anclem8  38392  areaquad  43984  mullimc  46373  mullimcf  46380  addlimc  46403  limclner  46406  stoweidlem5  46760  prproropf1olem2  48294  linc0scn0  49244  linc1  49246