Theorem ifcl 4570

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-if 4526

This theorem is referenced by:  ifcld  4571  ifcli  4572  ifpr  4692  suppr  9489  infpr  9521  ttukeylem3  10529  canthp1lem2  10671  xrmaxlt  13187  xrltmin  13188  xrmaxle  13189  xrlemin  13190  lemaxle  13201  z2ge  13204  ixxin  13368  uzsup  13855  expmulnbnd  14224  discr1  14228  uzin2  15318  rexanre  15320  caubnd  15332  limsupbnd2  15454  rlimcn3  15561  reccn2  15568  lo1mul  15599  rlimno1  15627  fsumsplit  15714  isumless  15818  explecnv  15838  cvgrat  15856  fprodsplit  15937  rpnnen2lem2  16186  sadadd2lem2  16419  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  smumullem  16461  pcmpt2  16856  prmreclem4  16882  prmreclem5  16883  prmreclem6  16884  1arith  16890  ressval  17206  acsfn  17633  mplcoe3  21970  mplcoe5  21972  ordtbaslem  23086  pnfnei  23118  mnfnei  23119  uzrest  23795  fclsval  23906  blin  24321  blin2  24329  stdbdxmet  24418  nrginvrcnlem  24602  qtopbaslem  24669  metnrmlem1a  24768  metnrmlem1  24769  addcnlem  24774  evth  24879  xlebnum  24885  minveclem3b  25350  ovolicc1  25439  ismbfd  25562  mbfposr  25575  mbfi1fseqlem4  25642  mbfi1fseqlem5  25643  mbfi1flimlem  25646  itg2const  25664  itg2const2  25665  itg2splitlem  25672  itg2monolem3  25676  itg2gt0  25684  itg2cnlem1  25685  itg2cnlem2  25686  itg2cn  25687  iblre  25717  itgreval  25720  itgneg  25727  iblss  25728  itgitg1  25732  itgle  25733  itgeqa  25737  itgss3  25738  itgless  25740  iblconst  25741  itgconst  25742  ibladdlem  25743  itgaddlem2  25747  iblabslem  25751  iblabsr  25753  iblmulc2  25754  itgmulc2lem2  25756  itgsplit  25759  bddiblnc  25765  dveflem  25905  elply2  26124  ply1term  26132  plyeq0lem  26138  plypf1  26140  coe1termlem  26186  coe1term  26187  aalioulem5  26265  aalioulem6  26266  cxpcn3lem  26676  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  30042  resvval  33033  signspval  34179  signswmnd  34184  mblfinlem2  37126  mbfposadd  37135  cnambfre  37136  itg2addnclem  37139  itg2addnc  37142  itg2gt0cn  37143  ibladdnclem  37144  itgaddnclem2  37147  iblabsnclem  37151  iblmulc2nc  37153  itgmulc2nclem2  37155  ftc1anclem5  37165  ftc1anclem7  37167  ftc1anclem8  37168  areaquad  42635  mullimc  44995  mullimcf  45002  addlimc  45027  limclner  45030  stoweidlem5  45384  prproropf1olem2  46835  linc0scn0  47482  linc1  47484

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »