Theorem ifcl 4509

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4465

This theorem is referenced by:  ifcld  4510  ifcli  4511  ifpr  4632  suppr  9191  infpr  9223  ttukeylem3  10251  canthp1lem2  10393  xrmaxlt  12897  xrltmin  12898  xrmaxle  12899  xrlemin  12900  lemaxle  12911  z2ge  12914  ixxin  13078  uzsup  13564  expmulnbnd  13931  discr1  13935  uzin2  15037  rexanre  15039  caubnd  15051  limsupbnd2  15173  rlimcn3  15280  reccn2  15287  lo1mul  15318  rlimno1  15346  fsumsplit  15434  isumless  15538  explecnv  15558  cvgrat  15576  fprodsplit  15657  rpnnen2lem2  15905  sadadd2lem2  16138  sadcaddlem  16145  sadadd2lem  16147  sadadd3  16149  smumullem  16180  pcmpt2  16575  prmreclem4  16601  prmreclem5  16602  prmreclem6  16603  1arith  16609  ressval  16925  acsfn  17349  mplcoe3  21220  mplcoe5  21222  ordtbaslem  22320  pnfnei  22352  mnfnei  22353  uzrest  23029  fclsval  23140  blin  23555  blin2  23563  stdbdxmet  23652  nrginvrcnlem  23836  qtopbaslem  23903  metnrmlem1a  24002  metnrmlem1  24003  addcnlem  24008  evth  24103  xlebnum  24109  minveclem3b  24573  ovolicc1  24661  ismbfd  24784  mbfposr  24797  mbfi1fseqlem4  24864  mbfi1fseqlem5  24865  mbfi1flimlem  24868  itg2const  24886  itg2const2  24887  itg2splitlem  24894  itg2monolem3  24898  itg2gt0  24906  itg2cnlem1  24907  itg2cnlem2  24908  itg2cn  24909  iblre  24939  itgreval  24942  itgneg  24949  iblss  24950  itgitg1  24954  itgle  24955  itgeqa  24959  itgss3  24960  itgless  24962  iblconst  24963  itgconst  24964  ibladdlem  24965  itgaddlem2  24969  iblabslem  24973  iblabsr  24975  iblmulc2  24976  itgmulc2lem2  24978  itgsplit  24981  bddiblnc  24987  dveflem  25124  elply2  25338  ply1term  25346  plyeq0lem  25352  plypf1  25354  coe1termlem  25400  coe1term  25401  aalioulem5  25477  aalioulem6  25478  cxpcn3lem  25881  o1cxp  26105  cxp2lim  26107  cxploglim  26108  cxploglim2  26109  ftalem1  26203  ftalem2  26204  ftalem4  26206  muf  26270  chtdif  26288  ppidif  26293  prmorcht  26308  muinv  26323  chtppilim  26604  rplogsumlem2  26614  dchrvmasumiflem1  26630  dchrvmasumiflem2  26631  rpvmasum2  26641  rplogsum  26656  ostth2lem2  26763  ostth2lem3  26764  ostth2lem4  26765  eupth2lems  28581  resvval  31505  signspval  32510  signswmnd  32515  mblfinlem2  35794  mbfposadd  35803  cnambfre  35804  itg2addnclem  35807  itg2addnc  35810  itg2gt0cn  35811  ibladdnclem  35812  itgaddnclem2  35815  iblabsnclem  35819  iblmulc2nc  35821  itgmulc2nclem2  35823  ftc1anclem5  35833  ftc1anclem7  35835  ftc1anclem8  35836  areaquad  41027  mullimc  43111  mullimcf  43118  addlimc  43143  limclner  43146  stoweidlem5  43500  prproropf1olem2  44908  linc0scn0  45716  linc1  45718