Theorem ifcl 4571

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ifcif 4525

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifcld  4572  ifcli  4573  ifpr  4693  suppr  9511  infpr  9543  ttukeylem3  10551  canthp1lem2  10693  xrmaxlt  13223  xrltmin  13224  xrmaxle  13225  xrlemin  13226  lemaxle  13237  z2ge  13240  ixxin  13404  uzsup  13903  expmulnbnd  14274  discr1  14278  uzin2  15383  rexanre  15385  caubnd  15397  limsupbnd2  15519  rlimcn3  15626  reccn2  15633  lo1mul  15664  rlimno1  15690  fsumsplit  15777  isumless  15881  explecnv  15901  cvgrat  15919  fprodsplit  16002  rpnnen2lem2  16251  sadadd2lem2  16487  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  smumullem  16529  pcmpt2  16931  prmreclem4  16957  prmreclem5  16958  prmreclem6  16959  1arith  16965  ressval  17277  acsfn  17702  mplcoe3  22056  mplcoe5  22058  ordtbaslem  23196  pnfnei  23228  mnfnei  23229  uzrest  23905  fclsval  24016  blin  24431  blin2  24439  stdbdxmet  24528  nrginvrcnlem  24712  qtopbaslem  24779  metnrmlem1a  24880  metnrmlem1  24881  addcnlem  24886  evth  24991  xlebnum  24997  minveclem3b  25462  ovolicc1  25551  ismbfd  25674  mbfposr  25687  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1flimlem  25757  itg2const  25775  itg2const2  25776  itg2splitlem  25783  itg2monolem3  25787  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  iblre  25829  itgreval  25832  itgneg  25839  iblss  25840  itgitg1  25844  itgle  25845  itgeqa  25849  itgss3  25850  itgless  25852  iblconst  25853  itgconst  25854  ibladdlem  25855  itgaddlem2  25859  iblabslem  25863  iblabsr  25865  iblmulc2  25866  itgmulc2lem2  25868  itgsplit  25871  bddiblnc  25877  dveflem  26017  elply2  26235  ply1term  26243  plyeq0lem  26249  plypf1  26251  coe1termlem  26297  coe1term  26298  aalioulem5  26378  aalioulem6  26379  cxpcn3lem  26790  o1cxp  27018  cxp2lim  27020  cxploglim  27021  cxploglim2  27022  ftalem1  27116  ftalem2  27117  ftalem4  27119  muf  27183  chtdif  27201  ppidif  27206  prmorcht  27221  muinv  27236  chtppilim  27519  rplogsumlem2  27529  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  rpvmasum2  27556  rplogsum  27571  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  eupth2lems  30257  resvval  33353  signspval  34567  signswmnd  34572  mblfinlem2  37665  mbfposadd  37674  cnambfre  37675  itg2addnclem  37678  itg2addnc  37681  itg2gt0cn  37682  ibladdnclem  37683  itgaddnclem2  37686  iblabsnclem  37690  iblmulc2nc  37692  itgmulc2nclem2  37694  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  areaquad  43228  mullimc  45631  mullimcf  45638  addlimc  45663  limclner  45666  stoweidlem5  46020  prproropf1olem2  47491  linc0scn0  48340  linc1  48342