Theorem ifcl 4527

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  ifcld  4528  ifcli  4529  ifpr  4650  suppr  9468  infpr  9501  ttukeylem3  10593  canthp1lem2  10742  xrmaxlt  13315  xrltmin  13316  xrmaxle  13317  xrlemin  13318  lemaxle  13329  z2ge  13332  ixxin  13497  uzsup  14007  expmulnbnd  14383  discr1  14387  uzin2  15518  rexanre  15520  caubnd  15532  limsupbnd2  15656  rlimcn3  15763  reccn2  15770  lo1mul  15801  rlimno1  15827  fsumsplit  15913  isumless  16020  explecnv  16040  cvgrat  16058  fprodsplit  16139  rpnnen2lem2  16389  sadadd2lem2  16626  sadcaddlem  16633  sadadd2lem  16635  sadadd3  16637  smumullem  16668  pcmpt2  17077  prmreclem4  17103  prmreclem5  17104  prmreclem6  17105  1arith  17111  ressval  17417  acsfn  17839  mplcoe3  22353  mplcoe5  22355  ordtbaslem  23512  pnfnei  23544  mnfnei  23545  uzrest  24222  fclsval  24333  blin  24746  blin2  24754  stdbdxmet  24840  nrginvrcnlem  25016  qtopbaslem  25083  metnrmlem1a  25184  metnrmlem1  25185  addcnlem  25190  evth  25286  xlebnum  25292  minveclem3b  25755  ovolicc1  25843  ismbfd  25966  mbfposr  25979  mbfi1fseqlem4  26045  mbfi1fseqlem5  26046  mbfi1flimlem  26049  itg2const  26067  itg2const2  26068  itg2splitlem  26075  itg2monolem3  26079  itg2gt0  26087  itg2cnlem1  26088  itg2cnlem2  26089  itg2cn  26090  iblre  26120  itgreval  26123  itgneg  26130  iblss  26131  itgitg1  26135  itgle  26136  itgeqa  26140  itgss3  26141  itgless  26143  iblconst  26144  itgconst  26145  ibladdlem  26146  itgaddlem2  26150  iblabslem  26154  iblabsr  26156  iblmulc2  26157  itgmulc2lem2  26159  itgsplit  26162  bddiblnc  26168  dveflem  26305  elply2  26520  ply1term  26528  plyeq0lem  26535  plypf1  26537  coe1termlem  26583  coe1term  26584  aalioulem5  26669  aalioulem6  26670  cxpcn3lem  27081  o1cxp  27308  cxp2lim  27310  cxploglim  27311  cxploglim2  27312  ftalem1  27406  ftalem2  27407  ftalem4  27409  muf  27473  chtdif  27491  ppidif  27496  prmorcht  27511  muinv  27526  chtppilim  27808  rplogsumlem2  27818  dchrvmasumiflem1  27834  dchrvmasumiflem2  27835  rpvmasum2  27845  rplogsum  27860  ostth2lem2  27967  ostth2lem3  27968  ostth2lem4  27969  eupth2lems  30845  resvval  33937  signspval  35228  signswmnd  35233  mblfinlem2  38670  mbfposadd  38679  cnambfre  38680  itg2addnclem  38683  itg2addnc  38686  itg2gt0cn  38687  ibladdnclem  38688  itgaddnclem2  38691  iblabsnclem  38695  iblmulc2nc  38697  itgmulc2nclem2  38699  ftc1anclem5  38709  ftc1anclem7  38711  ftc1anclem8  38712  areaquad  44312  mullimc  46722  mullimcf  46729  addlimc  46752  limclner  46755  stoweidlem5  47109  prproropf1olem2  48680  linc0scn0  49629  linc1  49631