Theorem ifcl 4524

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  ifcld  4525  ifcli  4526  ifpr  4647  suppr  9381  infpr  9414  ttukeylem3  10424  canthp1lem2  10566  xrmaxlt  13101  xrltmin  13102  xrmaxle  13103  xrlemin  13104  lemaxle  13115  z2ge  13118  ixxin  13283  uzsup  13785  expmulnbnd  14160  discr1  14164  uzin2  15270  rexanre  15272  caubnd  15284  limsupbnd2  15408  rlimcn3  15515  reccn2  15522  lo1mul  15553  rlimno1  15579  fsumsplit  15666  isumless  15770  explecnv  15790  cvgrat  15808  fprodsplit  15891  rpnnen2lem2  16142  sadadd2lem2  16379  sadcaddlem  16386  sadadd2lem  16388  sadadd3  16390  smumullem  16421  pcmpt2  16823  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arith  16857  ressval  17162  acsfn  17583  mplcoe3  21961  mplcoe5  21963  ordtbaslem  23091  pnfnei  23123  mnfnei  23124  uzrest  23800  fclsval  23911  blin  24325  blin2  24333  stdbdxmet  24419  nrginvrcnlem  24595  qtopbaslem  24662  metnrmlem1a  24763  metnrmlem1  24764  addcnlem  24769  evth  24874  xlebnum  24880  minveclem3b  25344  ovolicc1  25433  ismbfd  25556  mbfposr  25569  mbfi1fseqlem4  25635  mbfi1fseqlem5  25636  mbfi1flimlem  25639  itg2const  25657  itg2const2  25658  itg2splitlem  25665  itg2monolem3  25669  itg2gt0  25677  itg2cnlem1  25678  itg2cnlem2  25679  itg2cn  25680  iblre  25711  itgreval  25714  itgneg  25721  iblss  25722  itgitg1  25726  itgle  25727  itgeqa  25731  itgss3  25732  itgless  25734  iblconst  25735  itgconst  25736  ibladdlem  25737  itgaddlem2  25741  iblabslem  25745  iblabsr  25747  iblmulc2  25748  itgmulc2lem2  25750  itgsplit  25753  bddiblnc  25759  dveflem  25899  elply2  26117  ply1term  26125  plyeq0lem  26131  plypf1  26133  coe1termlem  26179  coe1term  26180  aalioulem5  26260  aalioulem6  26261  cxpcn3lem  26673  o1cxp  26901  cxp2lim  26903  cxploglim  26904  cxploglim2  26905  ftalem1  26999  ftalem2  27000  ftalem4  27002  muf  27066  chtdif  27084  ppidif  27089  prmorcht  27104  muinv  27119  chtppilim  27402  rplogsumlem2  27412  dchrvmasumiflem1  27428  dchrvmasumiflem2  27429  rpvmasum2  27439  rplogsum  27454  ostth2lem2  27561  ostth2lem3  27562  ostth2lem4  27563  eupth2lems  30200  resvval  33280  signspval  34522  signswmnd  34527  mblfinlem2  37640  mbfposadd  37649  cnambfre  37650  itg2addnclem  37653  itg2addnc  37656  itg2gt0cn  37657  ibladdnclem  37658  itgaddnclem2  37661  iblabsnclem  37665  iblmulc2nc  37667  itgmulc2nclem2  37669  ftc1anclem5  37679  ftc1anclem7  37681  ftc1anclem8  37682  areaquad  43192  mullimc  45601  mullimcf  45608  addlimc  45633  limclner  45636  stoweidlem5  45990  prproropf1olem2  47492  linc0scn0  48412  linc1  48414