Theorem ifcl 4575

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  ifcld  4576  ifcli  4577  ifpr  4697  suppr  9508  infpr  9540  ttukeylem3  10548  canthp1lem2  10690  xrmaxlt  13219  xrltmin  13220  xrmaxle  13221  xrlemin  13222  lemaxle  13233  z2ge  13236  ixxin  13400  uzsup  13899  expmulnbnd  14270  discr1  14274  uzin2  15379  rexanre  15381  caubnd  15393  limsupbnd2  15515  rlimcn3  15622  reccn2  15629  lo1mul  15660  rlimno1  15686  fsumsplit  15773  isumless  15877  explecnv  15897  cvgrat  15915  fprodsplit  15998  rpnnen2lem2  16247  sadadd2lem2  16483  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  smumullem  16525  pcmpt2  16926  prmreclem4  16952  prmreclem5  16953  prmreclem6  16954  1arith  16960  ressval  17276  acsfn  17703  mplcoe3  22073  mplcoe5  22075  ordtbaslem  23211  pnfnei  23243  mnfnei  23244  uzrest  23920  fclsval  24031  blin  24446  blin2  24454  stdbdxmet  24543  nrginvrcnlem  24727  qtopbaslem  24794  metnrmlem1a  24893  metnrmlem1  24894  addcnlem  24899  evth  25004  xlebnum  25010  minveclem3b  25475  ovolicc1  25564  ismbfd  25687  mbfposr  25700  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1flimlem  25771  itg2const  25789  itg2const2  25790  itg2splitlem  25797  itg2monolem3  25801  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  iblre  25843  itgreval  25846  itgneg  25853  iblss  25854  itgitg1  25858  itgle  25859  itgeqa  25863  itgss3  25864  itgless  25866  iblconst  25867  itgconst  25868  ibladdlem  25869  itgaddlem2  25873  iblabslem  25877  iblabsr  25879  iblmulc2  25880  itgmulc2lem2  25882  itgsplit  25885  bddiblnc  25891  dveflem  26031  elply2  26249  ply1term  26257  plyeq0lem  26263  plypf1  26265  coe1termlem  26311  coe1term  26312  aalioulem5  26392  aalioulem6  26393  cxpcn3lem  26804  o1cxp  27032  cxp2lim  27034  cxploglim  27035  cxploglim2  27036  ftalem1  27130  ftalem2  27131  ftalem4  27133  muf  27197  chtdif  27215  ppidif  27220  prmorcht  27235  muinv  27250  chtppilim  27533  rplogsumlem2  27543  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  rpvmasum2  27570  rplogsum  27585  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  eupth2lems  30266  resvval  33332  signspval  34545  signswmnd  34550  mblfinlem2  37644  mbfposadd  37653  cnambfre  37654  itg2addnclem  37657  itg2addnc  37660  itg2gt0cn  37661  ibladdnclem  37662  itgaddnclem2  37665  iblabsnclem  37669  iblmulc2nc  37671  itgmulc2nclem2  37673  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  areaquad  43204  mullimc  45571  mullimcf  45578  addlimc  45603  limclner  45606  stoweidlem5  45960  prproropf1olem2  47428  linc0scn0  48268  linc1  48270