Theorem ifcl 4531

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  ifcld  4532  ifcli  4533  ifpr  4654  suppr  9494  infpr  9527  ttukeylem3  10619  canthp1lem2  10768  xrmaxlt  13341  xrltmin  13342  xrmaxle  13343  xrlemin  13344  lemaxle  13355  z2ge  13358  ixxin  13523  uzsup  14033  expmulnbnd  14409  discr1  14413  uzin2  15544  rexanre  15546  caubnd  15558  limsupbnd2  15682  rlimcn3  15789  reccn2  15796  lo1mul  15827  rlimno1  15853  fsumsplit  15939  isumless  16046  explecnv  16066  cvgrat  16084  fprodsplit  16165  rpnnen2lem2  16415  sadadd2lem2  16652  sadcaddlem  16659  sadadd2lem  16661  sadadd3  16663  smumullem  16694  pcmpt2  17103  prmreclem4  17129  prmreclem5  17130  prmreclem6  17131  1arith  17137  ressval  17443  acsfn  17865  mplcoe3  22380  mplcoe5  22382  ordtbaslem  23539  pnfnei  23571  mnfnei  23572  uzrest  24249  fclsval  24360  blin  24773  blin2  24781  stdbdxmet  24867  nrginvrcnlem  25043  qtopbaslem  25110  metnrmlem1a  25211  metnrmlem1  25212  addcnlem  25217  evth  25313  xlebnum  25319  minveclem3b  25782  ovolicc1  25870  ismbfd  25993  mbfposr  26006  mbfi1fseqlem4  26072  mbfi1fseqlem5  26073  mbfi1flimlem  26076  itg2const  26094  itg2const2  26095  itg2splitlem  26102  itg2monolem3  26106  itg2gt0  26114  itg2cnlem1  26115  itg2cnlem2  26116  itg2cn  26117  iblre  26147  itgreval  26150  itgneg  26157  iblss  26158  itgitg1  26162  itgle  26163  itgeqa  26167  itgss3  26168  itgless  26170  iblconst  26171  itgconst  26172  ibladdlem  26173  itgaddlem2  26177  iblabslem  26181  iblabsr  26183  iblmulc2  26184  itgmulc2lem2  26186  itgsplit  26189  bddiblnc  26195  dveflem  26332  elply2  26547  ply1term  26555  plyeq0lem  26562  plypf1  26564  coe1termlem  26610  coe1term  26611  aalioulem5  26696  aalioulem6  26697  cxpcn3lem  27108  o1cxp  27335  cxp2lim  27337  cxploglim  27338  cxploglim2  27339  ftalem1  27433  ftalem2  27434  ftalem4  27436  muf  27500  chtdif  27518  ppidif  27523  prmorcht  27538  muinv  27553  chtppilim  27835  rplogsumlem2  27845  dchrvmasumiflem1  27861  dchrvmasumiflem2  27862  rpvmasum2  27872  rplogsum  27887  ostth2lem2  27994  ostth2lem3  27995  ostth2lem4  27996  eupth2lems  30872  resvval  33974  signspval  35264  signswmnd  35269  mblfinlem2  38781  mbfposadd  38790  cnambfre  38791  itg2addnclem  38794  itg2addnc  38797  itg2gt0cn  38798  ibladdnclem  38799  itgaddnclem2  38802  iblabsnclem  38806  iblmulc2nc  38808  itgmulc2nclem2  38810  ftc1anclem5  38820  ftc1anclem7  38822  ftc1anclem8  38823  areaquad  44421  mullimc  46843  mullimcf  46850  addlimc  46873  limclner  46876  stoweidlem5  47230  prproropf1olem2  48801  linc0scn0  49750  linc1  49752