Theorem ifcl 4523

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  ifcld  4524  ifcli  4525  ifpr  4649  suppr  9411  infpr  9444  ttukeylem3  10461  canthp1lem2  10604  xrmaxlt  13177  xrltmin  13178  xrmaxle  13179  xrlemin  13180  lemaxle  13191  z2ge  13194  ixxin  13359  uzsup  13866  expmulnbnd  14241  discr1  14245  uzin2  15362  rexanre  15364  caubnd  15376  limsupbnd2  15500  rlimcn3  15607  reccn2  15614  lo1mul  15645  rlimno1  15671  fsumsplit  15758  isumless  15865  explecnv  15885  cvgrat  15903  fprodsplit  15986  rpnnen2lem2  16237  sadadd2lem2  16474  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  smumullem  16516  pcmpt2  16919  prmreclem4  16945  prmreclem5  16946  prmreclem6  16947  1arith  16953  ressval  17259  acsfn  17681  mplcoe3  22078  mplcoe5  22080  ordtbaslem  23235  pnfnei  23267  mnfnei  23268  uzrest  23944  fclsval  24055  blin  24468  blin2  24476  stdbdxmet  24562  nrginvrcnlem  24738  qtopbaslem  24805  metnrmlem1a  24906  metnrmlem1  24907  addcnlem  24912  evth  25008  xlebnum  25014  minveclem3b  25477  ovolicc1  25565  ismbfd  25688  mbfposr  25701  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  26028  elply2  26243  ply1term  26251  plyeq0lem  26257  plypf1  26259  coe1termlem  26305  coe1term  26306  aalioulem5  26387  aalioulem6  26388  cxpcn3lem  26799  o1cxp  27026  cxp2lim  27028  cxploglim  27029  cxploglim2  27030  ftalem1  27124  ftalem2  27125  ftalem4  27127  muf  27191  chtdif  27209  ppidif  27214  prmorcht  27229  muinv  27244  chtppilim  27526  rplogsumlem2  27536  dchrvmasumiflem1  27552  dchrvmasumiflem2  27553  rpvmasum2  27563  rplogsum  27578  ostth2lem2  27685  ostth2lem3  27686  ostth2lem4  27687  eupth2lems  30396  resvval  33475  signspval  34806  signswmnd  34811  mblfinlem2  38117  mbfposadd  38126  cnambfre  38127  itg2addnclem  38130  itg2addnc  38133  itg2gt0cn  38134  ibladdnclem  38135  itgaddnclem2  38138  iblabsnclem  38142  iblmulc2nc  38144  itgmulc2nclem2  38146  ftc1anclem5  38156  ftc1anclem7  38158  ftc1anclem8  38159  areaquad  43753  mullimc  46152  mullimcf  46159  addlimc  46182  limclner  46185  stoweidlem5  46539  prproropf1olem2  48070  linc0scn0  49005  linc1  49007